let p be autonomic FinPartState of SCM+FSA ; :: thesis: ( DataPart p <> {} implies IC SCM+FSA in dom p )
assume
DataPart p <> {}
; :: thesis: IC SCM+FSA in dom p
then A1:
dom (DataPart p) <> {}
;
assume
not IC SCM+FSA in dom p
; :: thesis: contradiction
then A2:
dom p misses {(IC SCM+FSA )}
by ZFMISC_1:56;
not p is autonomic
proof
consider d1 being
Element of
dom (DataPart p);
A3:
d1 in dom (DataPart p)
by A1;
dom (DataPart p) c= the
carrier of
SCM+FSA
by AMI_1:80;
then reconsider d1 =
d1 as
Element of
SCM+FSA by A3;
A4:
dom (DataPart p) c= Int-Locations \/ FinSeq-Locations
by RELAT_1:87, SCMFSA_2:127;
consider d2 being
Element of
Int-Locations \ (dom p);
not
Int-Locations c= dom p
;
then A5:
Int-Locations \ (dom p) <> {}
by XBOOLE_1:37;
then
d2 in Int-Locations
by XBOOLE_0:def 5;
then reconsider d2 =
d2 as
Int-Location by SCMFSA_2:11;
consider il being
Element of
NAT \ (dom p);
not
NAT c= dom p
;
then A6:
NAT \ (dom p) <> {}
by XBOOLE_1:37;
then
il in NAT
by XBOOLE_0:def 5;
then reconsider il =
il as
Instruction-Location of
SCM+FSA by AMI_1:def 4;
per cases
( d1 in Int-Locations or d1 in FinSeq-Locations )
by A3, A4, XBOOLE_0:def 3;
suppose
d1 in Int-Locations
;
:: thesis: not p is autonomic then reconsider d1 =
d1 as
Int-Location by SCMFSA_2:11;
set p1 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il));
set p2 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il));
consider s1 being
State of
SCM+FSA such that A7:
p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) c= s1
by CARD_3:97;
consider s2 being
State of
SCM+FSA such that A8:
p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) c= s2
by CARD_3:97;
take
s1
;
:: according to AMI_1:def 25 :: thesis: ex b1 being Element of K251(the Object-Kind of SCM+FSA ) st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Computation s1,b2) | (dom p) = (Computation b1,b2) | (dom p) )take
s2
;
:: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
not
d2 in dom p
by A5, XBOOLE_0:def 5;
then A9:
dom p misses {d2}
by ZFMISC_1:56;
not
il in dom p
by A6, XBOOLE_0:def 5;
then A10:
dom p misses {il}
by ZFMISC_1:56;
dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> 0 ))) \/ (dom (Start-At il))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC SCM+FSA )})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A2, XBOOLE_0:def 7
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A9, XBOOLE_0:def 7
.=
{}
by A10, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s1
by A7, XBOOLE_1:1;
:: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) ) dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ (dom (Start-At il))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC SCM+FSA )})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A2, XBOOLE_0:def 7
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A9, XBOOLE_0:def 7
.=
{}
by A10, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s2
by A8, XBOOLE_1:1;
:: thesis: not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p)take
1
;
:: thesis: not (Computation s1,1) | (dom p) = (Computation s2,1) | (dom p)
DataPart p c= p
by RELAT_1:88;
then A11:
dom (DataPart p) c= dom p
by RELAT_1:25;
dom (Computation s1,1) = the
carrier of
SCM+FSA
by AMI_1:79;
then A12:
dom ((Computation s1,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A13:
dom (Start-At il) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A14:
IC SCM+FSA in dom (Start-At il)
by TARSKI:def 1;
A15:
dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) = (dom ((il .--> (d1 := d2)) +* (d2 .--> 0 ))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A16:
IC SCM+FSA in dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A14, XBOOLE_0:def 3;
A17:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC SCM+FSA in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A16, XBOOLE_0:def 3;
then A18:
IC s1 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))) . (IC SCM+FSA )
by A7, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) . (IC SCM+FSA )
by A16, FUNCT_4:14
.=
(Start-At il) . (IC SCM+FSA )
by A14, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then A19:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
A20:
dom (d2 .--> 0 ) = {d2}
by FUNCOP_1:19;
il <> d2
by SCMFSA_2:84;
then A21:
not
il in dom (d2 .--> 0 )
by A20, TARSKI:def 1;
A22:
dom ((il .--> (d1 := d2)) +* (d2 .--> 0 )) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 0 ))
by FUNCT_4:def 1;
then A23:
il in dom ((il .--> (d1 := d2)) +* (d2 .--> 0 ))
by A19, XBOOLE_0:def 3;
il <> IC SCM+FSA
by AMI_1:48;
then A24:
not
il in dom (Start-At il)
by A13, TARSKI:def 1;
A25:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A15, A23, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A17, XBOOLE_0:def 3;
then A26:
s1 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))) . il
by A7, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) . il
by A25, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 0 )) . il
by A24, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A21, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A27:
d2 in dom (d2 .--> 0 )
by A20, TARSKI:def 1;
then A28:
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> 0 ))
by A22, XBOOLE_0:def 3;
d2 <> IC SCM+FSA
by SCMFSA_2:81;
then A29:
not
d2 in dom (Start-At il)
by A13, TARSKI:def 1;
A30:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A15, A28, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A17, XBOOLE_0:def 3;
then A31:
s1 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il))) . d2
by A7, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 0 )) +* (Start-At il)) . d2
by A30, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 0 )) . d2
by A29, FUNCT_4:12
.=
(d2 .--> 0 ) . d2
by A27, FUNCT_4:14
.=
0
by FUNCOP_1:87
;
(Computation s1,(0 + 1)) . d1 =
(Following (Computation s1,0 )) . d1
by AMI_1:14
.=
(Following s1) . d1
by AMI_1:13
.=
0
by A18, A26, A31, SCMFSA_2:89
;
then A32:
((Computation s1,1) | (dom p)) . d1 = 0
by A3, A11, A12, FUNCT_1:70;
dom (Computation s2,1) = the
carrier of
SCM+FSA
by AMI_1:79;
then A33:
dom ((Computation s2,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A34:
dom (Start-At il) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A35:
IC SCM+FSA in dom (Start-At il)
by TARSKI:def 1;
A36:
dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) = (dom ((il .--> (d1 := d2)) +* (d2 .--> 1))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A37:
IC SCM+FSA in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))
by A35, XBOOLE_0:def 3;
A38:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC SCM+FSA in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A37, XBOOLE_0:def 3;
then A39:
IC s2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))) . (IC SCM+FSA )
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) . (IC SCM+FSA )
by A37, FUNCT_4:14
.=
(Start-At il) . (IC SCM+FSA )
by A35, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then A40:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
A41:
dom (d2 .--> 1) = {d2}
by FUNCOP_1:19;
il <> d2
by SCMFSA_2:84;
then A42:
not
il in dom (d2 .--> 1)
by A41, TARSKI:def 1;
A43:
dom ((il .--> (d1 := d2)) +* (d2 .--> 1)) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> 1))
by FUNCT_4:def 1;
then A44:
il in dom ((il .--> (d1 := d2)) +* (d2 .--> 1))
by A40, XBOOLE_0:def 3;
il <> IC SCM+FSA
by AMI_1:48;
then A45:
not
il in dom (Start-At il)
by A34, TARSKI:def 1;
A46:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))
by A36, A44, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A38, XBOOLE_0:def 3;
then A47:
s2 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))) . il
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) . il
by A46, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 1)) . il
by A45, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A42, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A48:
d2 in dom (d2 .--> 1)
by A41, TARSKI:def 1;
then A49:
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> 1))
by A43, XBOOLE_0:def 3;
d2 <> IC SCM+FSA
by SCMFSA_2:81;
then A50:
not
d2 in dom (Start-At il)
by A34, TARSKI:def 1;
A51:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))
by A36, A49, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A38, XBOOLE_0:def 3;
then A52:
s2 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il))) . d2
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> 1)) +* (Start-At il)) . d2
by A51, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> 1)) . d2
by A50, FUNCT_4:12
.=
(d2 .--> 1) . d2
by A48, FUNCT_4:14
.=
1
by FUNCOP_1:87
;
(Computation s2,(0 + 1)) . d1 =
(Following (Computation s2,0 )) . d1
by AMI_1:14
.=
(Following s2) . d1
by AMI_1:13
.=
1
by A39, A47, A52, SCMFSA_2:89
;
hence
(Computation s1,1) | (dom p) <> (Computation s2,1) | (dom p)
by A3, A11, A32, A33, FUNCT_1:70;
:: thesis: verum end; suppose
d1 in FinSeq-Locations
;
:: thesis: not p is autonomic then reconsider d1 =
d1 as
FinSeq-Location by SCMFSA_2:12;
set p1 =
p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il));
set p2 =
p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il));
consider s1 being
State of
SCM+FSA such that A53:
p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) c= s1
by CARD_3:97;
consider s2 being
State of
SCM+FSA such that A54:
p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) c= s2
by CARD_3:97;
take
s1
;
:: according to AMI_1:def 25 :: thesis: ex b1 being Element of K251(the Object-Kind of SCM+FSA ) st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Computation s1,b2) | (dom p) = (Computation b1,b2) | (dom p) )take
s2
;
:: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
not
d2 in dom p
by A5, XBOOLE_0:def 5;
then A55:
dom p misses {d2}
by ZFMISC_1:56;
not
il in dom p
by A6, XBOOLE_0:def 5;
then A56:
dom p misses {il}
by ZFMISC_1:56;
dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) =
(dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 ))) \/ (dom (Start-At il))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 :=<0,...,0> d2))) \/ (dom (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 0 ))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC SCM+FSA )})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A2, XBOOLE_0:def 7
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A55, XBOOLE_0:def 7
.=
{}
by A56, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s1
by A53, XBOOLE_1:1;
:: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) ) dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) =
(dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1))) \/ (dom (Start-At il))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
((dom (il .--> (d1 :=<0,...,0> d2))) \/ (dom (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> 1))) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC SCM+FSA )}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC SCM+FSA )})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A2, XBOOLE_0:def 7
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A55, XBOOLE_0:def 7
.=
{}
by A56, XBOOLE_0:def 7
;
then
dom p misses dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s2
by A54, XBOOLE_1:1;
:: thesis: not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p)take
1
;
:: thesis: not (Computation s1,1) | (dom p) = (Computation s2,1) | (dom p)
DataPart p c= p
by RELAT_1:88;
then A57:
dom (DataPart p) c= dom p
by RELAT_1:25;
dom (Computation s1,1) = the
carrier of
SCM+FSA
by AMI_1:79;
then A58:
dom ((Computation s1,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A59:
dom (Start-At il) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A60:
IC SCM+FSA in dom (Start-At il)
by TARSKI:def 1;
A61:
dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) = (dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 ))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A62:
IC SCM+FSA in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A60, XBOOLE_0:def 3;
A63:
dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC SCM+FSA in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A62, XBOOLE_0:def 3;
then A64:
IC s1 =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))) . (IC SCM+FSA )
by A53, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) . (IC SCM+FSA )
by A62, FUNCT_4:14
.=
(Start-At il) . (IC SCM+FSA )
by A60, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 :=<0,...,0> d2)) = {il}
by FUNCOP_1:19;
then A65:
il in dom (il .--> (d1 :=<0,...,0> d2))
by TARSKI:def 1;
A66:
dom (d2 .--> 0 ) = {d2}
by FUNCOP_1:19;
il <> d2
by SCMFSA_2:84;
then A67:
not
il in dom (d2 .--> 0 )
by A66, TARSKI:def 1;
A68:
dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) = (dom (il .--> (d1 :=<0,...,0> d2))) \/ (dom (d2 .--> 0 ))
by FUNCT_4:def 1;
then A69:
il in dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 ))
by A65, XBOOLE_0:def 3;
il <> IC SCM+FSA
by AMI_1:48;
then A70:
not
il in dom (Start-At il)
by A59, TARSKI:def 1;
A71:
il in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A61, A69, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A63, XBOOLE_0:def 3;
then A72:
s1 . il =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))) . il
by A53, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) . il
by A71, FUNCT_4:14
.=
((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) . il
by A70, FUNCT_4:12
.=
(il .--> (d1 :=<0,...,0> d2)) . il
by A67, FUNCT_4:12
.=
d1 :=<0,...,0> d2
by FUNCOP_1:87
;
A73:
d2 in dom (d2 .--> 0 )
by A66, TARSKI:def 1;
then A74:
d2 in dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 ))
by A68, XBOOLE_0:def 3;
d2 <> IC SCM+FSA
by SCMFSA_2:81;
then A75:
not
d2 in dom (Start-At il)
by A59, TARSKI:def 1;
A76:
d2 in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))
by A61, A74, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)))
by A63, XBOOLE_0:def 3;
then A77:
s1 . d2 =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il))) . d2
by A53, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) +* (Start-At il)) . d2
by A76, FUNCT_4:14
.=
((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 0 )) . d2
by A75, FUNCT_4:12
.=
(d2 .--> 0 ) . d2
by A73, FUNCT_4:14
.=
0
by FUNCOP_1:87
;
consider k being
Element of
NAT such that A78:
k = abs (s1 . d2)
and A79:
(Exec (d1 :=<0,...,0> d2),s1) . d1 = k |-> 0
by SCMFSA_2:101;
A80:
k |-> 0 =
0 |-> 0
by A77, A78, ABSVALUE:7
.=
{}
by FINSEQ_2:72
;
(Computation s1,(0 + 1)) . d1 =
(Following (Computation s1,0 )) . d1
by AMI_1:14
.=
(Following s1) . d1
by AMI_1:13
.=
{}
by A64, A72, A79, A80
;
then A81:
((Computation s1,1) | (dom p)) . d1 = {}
by A3, A57, A58, FUNCT_1:70;
dom (Computation s2,1) = the
carrier of
SCM+FSA
by AMI_1:79;
then A82:
dom ((Computation s2,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A83:
dom (Start-At il) = {(IC SCM+FSA )}
by FUNCOP_1:19;
then A84:
IC SCM+FSA in dom (Start-At il)
by TARSKI:def 1;
A85:
dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) = (dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A86:
IC SCM+FSA in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))
by A84, XBOOLE_0:def 3;
A87:
dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC SCM+FSA in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A86, XBOOLE_0:def 3;
then A88:
IC s2 =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))) . (IC SCM+FSA )
by A54, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) . (IC SCM+FSA )
by A86, FUNCT_4:14
.=
(Start-At il) . (IC SCM+FSA )
by A84, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 :=<0,...,0> d2)) = {il}
by FUNCOP_1:19;
then A89:
il in dom (il .--> (d1 :=<0,...,0> d2))
by TARSKI:def 1;
A90:
dom (d2 .--> 1) = {d2}
by FUNCOP_1:19;
il <> d2
by SCMFSA_2:84;
then A91:
not
il in dom (d2 .--> 1)
by A90, TARSKI:def 1;
A92:
dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) = (dom (il .--> (d1 :=<0,...,0> d2))) \/ (dom (d2 .--> 1))
by FUNCT_4:def 1;
then A93:
il in dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1))
by A89, XBOOLE_0:def 3;
il <> IC SCM+FSA
by AMI_1:48;
then A94:
not
il in dom (Start-At il)
by A83, TARSKI:def 1;
A95:
il in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))
by A85, A93, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A87, XBOOLE_0:def 3;
then A96:
s2 . il =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))) . il
by A54, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) . il
by A95, FUNCT_4:14
.=
((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) . il
by A94, FUNCT_4:12
.=
(il .--> (d1 :=<0,...,0> d2)) . il
by A91, FUNCT_4:12
.=
d1 :=<0,...,0> d2
by FUNCOP_1:87
;
A97:
d2 in dom (d2 .--> 1)
by A90, TARSKI:def 1;
then A98:
d2 in dom ((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1))
by A92, XBOOLE_0:def 3;
d2 <> IC SCM+FSA
by SCMFSA_2:81;
then A99:
not
d2 in dom (Start-At il)
by A83, TARSKI:def 1;
A100:
d2 in dom (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))
by A85, A98, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)))
by A87, XBOOLE_0:def 3;
then A101:
s2 . d2 =
(p +* (((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il))) . d2
by A54, GRFUNC_1:8
.=
(((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) +* (Start-At il)) . d2
by A100, FUNCT_4:14
.=
((il .--> (d1 :=<0,...,0> d2)) +* (d2 .--> 1)) . d2
by A99, FUNCT_4:12
.=
(d2 .--> 1) . d2
by A97, FUNCT_4:14
.=
1
by FUNCOP_1:87
;
consider k being
Element of
NAT such that A102:
k = abs (s2 . d2)
and A103:
(Exec (d1 :=<0,...,0> d2),s2) . d1 = k |-> 0
by SCMFSA_2:101;
A104:
k |-> 0 =
1
|-> 0
by A101, A102, ABSVALUE:def 1
.=
<*0 *>
by FINSEQ_2:73
;
(Computation s2,(0 + 1)) . d1 =
(Following (Computation s2,0 )) . d1
by AMI_1:14
.=
(Following s2) . d1
by AMI_1:13
.=
<*0 *>
by A88, A96, A103, A104
;
hence
(Computation s1,1) | (dom p) <> (Computation s2,1) | (dom p)
by A3, A57, A81, A82, FUNCT_1:70;
:: thesis: verum end;
end;
hence
contradiction
; :: thesis: verum