:: BOOLMARK semantic presentation
theorem Th1: :: BOOLMARK:1
theorem Th2: :: BOOLMARK:2
theorem Th3: :: BOOLMARK:3
proof
let c
1, c
2 be
set ;
let c
3 be
Function;
let c
4 be
set ;
assume that E4:
c
1 /\ c
2 = {}
and E5:
(c3 +* (c1 --> c4)) .: c
2 <> c
3 .: c
2
;
:: according to XBOOLE_0:def 7
E6:
dom (c3 +* (c1 --> c4)) = (dom c3) \/ (dom (c1 --> c4))
by FUNCT_4:def 1;
E7:
dom (c1 --> c4) = c
1
by FUNCOP_1:19;
E8:
not for b
1 being
set holds
( b
1 in (c3 +* (c1 --> c4)) .: c
2 iff b
1 in c
3 .: c
2 )
by E5, TARSKI:2;
now
per cases
not ( ( for b1 being set holds
not ( b1 in (c3 +* (c1 --> c4)) .: c2 & not b1 in c3 .: c2 ) ) & ( for b1 being set holds
not ( not b1 in (c3 +* (c1 --> c4)) .: c2 & b1 in c3 .: c2 ) ) )
by E8;
case
ex b
1 being
set st
( b
1 in (c3 +* (c1 --> c4)) .: c
2 & not b
1 in c
3 .: c
2 )
;
then consider c
5 being
set such that E9:
c
5 in (c3 +* (c1 --> c4)) .: c
2
and E10:
not c
5 in c
3 .: c
2
;
consider c
6 being
set such that E11:
c
6 in dom (c3 +* (c1 --> c4))
and E12:
c
6 in c
2
and E13:
c
5 = (c3 +* (c1 --> c4)) . c
6
by E9, FUNCT_1:def 12;
E14:
not c
6 in c
1
by E4, E12, XBOOLE_0:def 3;
then E15:
c
6 in dom c
3
by E6, E7, E11, XBOOLE_0:def 2;
c
5 = c
3 . c
6
by E7, E13, E14, FUNCT_4:12;
hence
not verum
by E10, E12, E15, FUNCT_1:def 12;
end;
case
ex b
1 being
set st
( not b
1 in (c3 +* (c1 --> c4)) .: c
2 & b
1 in c
3 .: c
2 )
;
then consider c
5 being
set such that E9:
not c
5 in (c3 +* (c1 --> c4)) .: c
2
and E10:
c
5 in c
3 .: c
2
;
consider c
6 being
set such that E11:
c
6 in dom c
3
and E12:
c
6 in c
2
and E13:
c
5 = c
3 . c
6
by E10, FUNCT_1:def 12;
E14:
not c
6 in c
1
by E4, E12, XBOOLE_0:def 3;
E15:
c
6 in dom (c3 +* (c1 --> c4))
by E6, E11, XBOOLE_0:def 2;
c
5 = (c3 +* (c1 --> c4)) . c
6
by E7, E13, E14, FUNCT_4:12;
hence
not verum
by E9, E12, E15, FUNCT_1:def 12;
end;
end;
hence
not verum
;
end;
:: deftheorem Def1 defines Bool_marks_of BOOLMARK:def 1 :
:: deftheorem Def2 defines is_firable_on BOOLMARK:def 2 :
:: deftheorem Def3 defines Firing BOOLMARK:def 3 :
:: deftheorem Def4 defines is_firable_on BOOLMARK:def 4 :
definition
let c
1 be
PT_net_Str ;
let c
2 be
Boolean_marking of c
1;
let c
3 be
FinSequence of the
Transitions of c
1;
func Firing c
3,c
2 -> Boolean_marking of a
1 means :
Def5:
:: BOOLMARK:def 5
a
4 = a
2 if a
3 = {} otherwise ex b
1 being
FinSequence of
Bool_marks_of a
1 st
(
len a
3 = len b
1 & a
4 = b
1 /. (len b1) & b
1 /. 1
= Firing (a3 /. 1),a
2 & ( for b
2 being
Nat holds
( b
2 < len a
3 & b
2 > 0 implies b
1 /. (b2 + 1) = Firing (a3 /. (b2 + 1)),
(b1 /. b2) ) ) );
existence
( not ( c3 = {} & ( for b1 being Boolean_marking of c1 holds
not b1 = c2 ) ) & not ( not c3 = {} & ( for b1 being Boolean_marking of c1
for b2 being FinSequence of Bool_marks_of c1 holds
not ( len c3 = len b2 & b1 = b2 /. (len b2) & b2 /. 1 = Firing (c3 /. 1),c2 & ( for b3 being Nat holds
( b3 < len c3 & b3 > 0 implies b2 /. (b3 + 1) = Firing (c3 /. (b3 + 1)),(b2 /. b3) ) ) ) ) ) )
proof
defpred S
1[
Nat] means for b
1 being
FinSequence of the
Transitions of c
1 holds
( a
1 = len b
1 implies ( not ( b
1 = {} & ( for b
2 being
Boolean_marking of c
1 holds
not b
2 = c
2 ) ) & not ( b
1 <> {} & ( for b
2 being
Boolean_marking of c
1for b
3 being
FinSequence of
Bool_marks_of c
1 holds
not (
len b
1 = len b
3 & b
2 = b
3 /. (len b3) & b
3 /. 1
= Firing (b1 /. 1),c
2 & ( for b
4 being
Nat holds
( b
4 < len b
1 & b
4 > 0 implies b
3 /. (b4 + 1) = Firing (b1 /. (b4 + 1)),
(b3 /. b4) ) ) ) ) ) ) );
E6:
S
1[0]
by FINSEQ_1:25;
E7:
now
let c
4 be
Nat;
assume E8:
S
1[c
4]
;
thus
S
1[c
4 + 1]
proof
let c
5 be
FinSequence of the
Transitions of c
1;
assume E9:
c
4 + 1
= len c
5
;
thus
not ( c
5 = {} & ( for b
1 being
Boolean_marking of c
1 holds
not b
1 = c
2 ) )
;
thus
not ( c
5 <> {} & ( for b
1 being
Boolean_marking of c
1for b
2 being
FinSequence of
Bool_marks_of c
1 holds
not (
len c
5 = len b
2 & b
1 = b
2 /. (len b2) & b
2 /. 1
= Firing (c5 /. 1),c
2 & ( for b
3 being
Nat holds
( b
3 < len c
5 & b
3 > 0 implies b
2 /. (b3 + 1) = Firing (c5 /. (b3 + 1)),
(b2 /. b3) ) ) ) ) )
proof
assume
c
5 <> {}
;
then
len c
5 <> 0
by FINSEQ_1:25;
then consider c
6 being
FinSequence of the
Transitions of c
1, c
7 being
transition of c
1 such that E10:
c
5 = c
6 ^ <*c7*>
by FINSEQ_2:22;
c
4 + 1
= (len c6) + 1
by E9, E10, FINSEQ_2:19;
then E11:
c
4 = len c
6
;
per cases
not ( not c6 = {} & not c6 <> {} )
;
suppose E12:
c
6 <> {}
;
then consider c
8 being
Boolean_marking of c
1, c
9 being
FinSequence of
Bool_marks_of c
1 such that E13:
len c
6 = len c
9
and E14:
c
8 = c
9 /. (len c9)
and E15:
c
9 /. 1
= Firing (c6 /. 1),c
2
and E16:
for b
1 being
Nat holds
( b
1 < len c
6 & b
1 > 0 implies c
9 /. (b1 + 1) = Firing (c6 /. (b1 + 1)),
(c9 /. b1) )
by E8, E11;
take c
10 =
Firing c
7,c
8;
take c
11 = c
9 ^ <*c10*>;
E17:
len c
11 =
(len c9) + (len <*c10*>)
by FINSEQ_1:35
.=
(len c9) + 1
by FINSEQ_1:57
;
E18:
len c
5 =
(len c6) + (len <*c7*>)
by E10, FINSEQ_1:35
.=
(len c6) + 1
by FINSEQ_1:57
;
hence
len c
5 = len c
11
by E13, E17;
thus
c
10 = c
11 /. (len c11)
by E17, FINSEQ_4:82;
len c
6 <> 0
by E12, FINSEQ_1:25;
then E19:
len c
6 > 0
by NAT_1:19;
then
0
+ 1
< (len c9) + 1
by E13, XREAL_1:8;
then E20:
1
<= len c
9
by NAT_1:38;
then E21:
1
in dom c
9
by FINSEQ_3:27;
0
+ 1
< (len c6) + 1
by E19, XREAL_1:8;
then
1
<= len c
6
by NAT_1:38;
then E22:
1
in dom c
6
by FINSEQ_3:27;
thus c
11 /. 1 =
c
9 /. 1
by E21, FINSEQ_4:83
.=
Firing (c5 /. 1),c
2
by E10, E15, E22, FINSEQ_4:83
;
let c
12 be
Nat;
assume that E23:
c
12 < len c
5
and E24:
c
12 > 0
;
thus
c
11 /. (c12 + 1) = Firing (c5 /. (c12 + 1)),
(c11 /. c12)
proof
E25:
Seg ((len c6) + 1) = (Seg (len c6)) \/ {((len c6) + 1)}
by FINSEQ_1:11;
E26:
1
<= c
12 + 1
by NAT_1:37;
c
12 + 1
<= (len c6) + 1
by E18, E23, NAT_1:38;
then E27:
c
12 + 1
in Seg ((len c6) + 1)
by E26, FINSEQ_1:3;
per cases
( c12 + 1 in Seg (len c6) or c12 + 1 in {((len c6) + 1)} )
by E25, E27, XBOOLE_0:def 2;
suppose E28:
c
12 + 1
in Seg (len c6)
;
then
c
12 + 1
<= len c
6
by FINSEQ_1:3;
then
c
12 < len c
6
by NAT_1:38;
then E29:
c
9 /. (c12 + 1) = Firing (c6 /. (c12 + 1)),
(c9 /. c12)
by E16, E24;
0
+ 1
< c
12 + 1
by E24, XREAL_1:8;
then E30:
1
<= c
12
by NAT_1:38;
c
12 + 1
in dom c
9
by E13, E28, FINSEQ_1:def 3;
then E31:
c
9 /. (c12 + 1) = c
11 /. (c12 + 1)
by FINSEQ_4:83;
E32:
c
12 + 1
<= len c
9
by E13, E28, FINSEQ_1:3;
c
12 + 1
in dom c
6
by E28, FINSEQ_1:def 3;
then E33:
c
6 /. (c12 + 1) = c
5 /. (c12 + 1)
by E10, FINSEQ_4:83;
c
12 + 1
<= (len c9) + 1
by E32, NAT_1:37;
then
c
12 <= len c
9
by XREAL_1:8;
then
c
12 in dom c
9
by E30, FINSEQ_3:27;
hence
c
11 /. (c12 + 1) = Firing (c5 /. (c12 + 1)),
(c11 /. c12)
by E29, E31, E33, FINSEQ_4:83;
end;
suppose
c
12 + 1
in {((len c6) + 1)}
;
then E28:
c
12 + 1
= (len c6) + 1
by TARSKI:def 1;
then E29:
c
12 = len c
6
;
E30:
c
11 /. (c12 + 1) = c
10
by E13, E28, FINSEQ_4:82;
E31:
c
5 /. (c12 + 1) = c
7
by E10, E28, FINSEQ_4:82;
len c
9 in dom c
9
by E20, FINSEQ_3:27;
hence
c
11 /. (c12 + 1) = Firing (c5 /. (c12 + 1)),
(c11 /. c12)
by E13, E14, E29, E30, E31, FINSEQ_4:83;
end;
end;
end;
end;
end;
end;
end;
end;
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E6, E7);
hence
( not ( c
3 = {} & ( for b
1 being
Boolean_marking of c
1 holds
not b
1 = c
2 ) ) & not ( not c
3 = {} & ( for b
1 being
Boolean_marking of c
1for b
2 being
FinSequence of
Bool_marks_of c
1 holds
not (
len c
3 = len b
2 & b
1 = b
2 /. (len b2) & b
2 /. 1
= Firing (c3 /. 1),c
2 & ( for b
3 being
Nat holds
( b
3 < len c
3 & b
3 > 0 implies b
2 /. (b3 + 1) = Firing (c3 /. (b3 + 1)),
(b2 /. b3) ) ) ) ) ) )
;
end;
uniqueness
for b1, b2 being Boolean_marking of c1 holds
( ( c3 = {} & b1 = c2 & b2 = c2 implies b1 = b2 ) & ( not c3 = {} & ex b3 being FinSequence of Bool_marks_of c1 st
( len c3 = len b3 & b1 = b3 /. (len b3) & b3 /. 1 = Firing (c3 /. 1),c2 & ( for b4 being Nat holds
( b4 < len c3 & b4 > 0 implies b3 /. (b4 + 1) = Firing (c3 /. (b4 + 1)),(b3 /. b4) ) ) ) & ex b3 being FinSequence of Bool_marks_of c1 st
( len c3 = len b3 & b2 = b3 /. (len b3) & b3 /. 1 = Firing (c3 /. 1),c2 & ( for b4 being Nat holds
( b4 < len c3 & b4 > 0 implies b3 /. (b4 + 1) = Firing (c3 /. (b4 + 1)),(b3 /. b4) ) ) ) implies b1 = b2 ) )
proof
let c
4, c
5 be
Boolean_marking of c
1;
thus
( c
3 = {} & c
4 = c
2 & c
5 = c
2 implies c
4 = c
5 )
;
assume
c
3 <> {}
;
given c
6 being
FinSequence of
Bool_marks_of c
1 such that E6:
len c
3 = len c
6
and E7:
c
4 = c
6 /. (len c6)
and E8:
c
6 /. 1
= Firing (c3 /. 1),c
2
and E9:
for b
1 being
Nat holds
( b
1 < len c
3 & b
1 > 0 implies c
6 /. (b1 + 1) = Firing (c3 /. (b1 + 1)),
(c6 /. b1) )
;
given c
7 being
FinSequence of
Bool_marks_of c
1 such that E10:
len c
3 = len c
7
and E11:
c
5 = c
7 /. (len c7)
and E12:
c
7 /. 1
= Firing (c3 /. 1),c
2
and E13:
for b
1 being
Nat holds
( b
1 < len c
3 & b
1 > 0 implies c
7 /. (b1 + 1) = Firing (c3 /. (b1 + 1)),
(c7 /. b1) )
;
defpred S
1[
Nat] means ( a
1 in Seg (len c3) implies c
6 /. a
1 = c
7 /. a
1 );
E14:
S
1[0]
by FINSEQ_1:3;
E15:
now
let c
8 be
Nat;
assume E16:
S
1[c
8]
;
now
assume E17:
c
8 + 1
in Seg (len c3)
;
per cases
not ( not c8 = 0 & not c8 <> 0 )
;
suppose E18:
c
8 <> 0
;
E19:
c
8 + 1
<= len c
3
by E17, FINSEQ_1:3;
E20:
c
8 < c
8 + 1
by XREAL_1:31;
then E21:
( c
8 > 0 & c
8 < len c
3 )
by E18, E19, XXREAL_0:2, NAT_1:19;
( 1
<= c
8 & c
8 <= len c
3 )
by E18, E19, E20, XXREAL_0:2, NAT_1:39;
hence c
6 /. (c8 + 1) =
Firing (c3 /. (c8 + 1)),
(c7 /. c8)
by E9, E16, E21, FINSEQ_1:3
.=
c
7 /. (c8 + 1)
by E13, E21
;
end;
end;
end;
hence
S
1[c
8 + 1]
;
end;
E16:
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E14, E15);
hence
c
4 = c
5
by E6, E7, E10, E11, FINSEQ_2:10;
end;
correctness
consistency
for b1 being Boolean_marking of c1 holds
verum;
;
end;
:: deftheorem Def5 defines Firing BOOLMARK:def 5 :
theorem Th4: :: BOOLMARK:4
canceled;
theorem Th5: :: BOOLMARK:5
theorem Th6: :: BOOLMARK:6