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