let R be good Ring; ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st DataPart p <> {} holds
IC (SCM R) in dom p )
assume A1:
not R is trivial
; for p being autonomic FinPartState of (SCM R) st DataPart p <> {} holds
IC (SCM R) in dom p
let p be autonomic FinPartState of (SCM R); ( DataPart p <> {} implies IC (SCM R) in dom p )
assume
DataPart p <> {}
; IC (SCM R) in dom p
then A2:
dom (DataPart p) <> {}
;
assume A3:
not IC (SCM R) in dom p
; contradiction
not p is autonomic
proof
consider il being
Element of
NAT \ (dom p);
consider d2 being
Element of
(Data-Locations SCM) \ (dom p);
consider d1 being
Element of
dom (DataPart p);
A4:
d1 in dom (DataPart p)
by A2;
dom (DataPart p) c= the
carrier of
(SCM R)
by RELAT_1:def 18;
then reconsider d1 =
d1 as
Element of
(SCM R) by A4;
not
Data-Locations SCM c= dom p
;
then A5:
(Data-Locations SCM) \ (dom p) <> {}
by XBOOLE_1:37;
then
d2 in Data-Locations SCM
by XBOOLE_0:def 5;
then reconsider d2 =
d2 as
Data-Location of
R by SCMRING2:1;
A6:
not
d2 in dom p
by A5, XBOOLE_0:def 5;
not
NAT c= dom p
;
then A7:
NAT \ (dom p) <> {}
by XBOOLE_1:37;
then reconsider il =
il as
Element of
NAT by XBOOLE_0:def 5;
A8:
not
il in dom p
by A7, XBOOLE_0:def 5;
Data-Locations (SCM R) = Data-Locations SCM
by SCMRING2:31;
then
dom (DataPart p) c= Data-Locations SCM
by RELAT_1:87;
then reconsider d1 =
d1 as
Data-Location of
R by A4, SCMRING2:1;
A9:
dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))) = (dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))) \/ (dom (Start-At (il,(SCM R))))
by FUNCT_4:def 1;
set p1 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))));
consider s1 being
State of
(SCM R) such that A10:
p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))) c= s1
by PBOOLE:156;
A11:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))))
by FUNCT_4:def 1;
A12:
dom (Start-At (il,(SCM R))) = {(IC (SCM R))}
by FUNCOP_1:19;
then A13:
IC (SCM R) in dom (Start-At (il,(SCM R)))
by TARSKI:def 1;
then A14:
IC (SCM R) in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))
by A9, XBOOLE_0:def 3;
then
IC (SCM R) in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))))
by A11, XBOOLE_0:def 3;
then A15:
IC s1 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))) . (IC (SCM R))
by A10, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))) . (IC (SCM R))
by A14, FUNCT_4:14
.=
(Start-At (il,(SCM R))) . (IC (SCM R))
by A13, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
A16:
il <> IC (SCM R)
by COMPOS_1:3;
then A17:
not
il in dom (Start-At (il,(SCM R)))
by A12, TARSKI:def 1;
A18:
dom (Start-At (il,(SCM R))) = {(IC (SCM R))}
by FUNCOP_1:19;
then A19:
not
il in dom (Start-At (il,(SCM R)))
by A16, TARSKI:def 1;
A20:
d2 <> IC (SCM R)
by SCMRING3:3;
then A21:
not
d2 in dom (Start-At (il,(SCM R)))
by A12, TARSKI:def 1;
A22:
not
d2 in dom (Start-At (il,(SCM R)))
by A20, A18, TARSKI:def 1;
A23:
dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R))) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> (0. R)))
by FUNCT_4:def 1;
A24:
dom (d2 .--> (0. R)) = {d2}
by FUNCOP_1:19;
then A25:
d2 in dom (d2 .--> (0. R))
by TARSKI:def 1;
then
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))
by A23, XBOOLE_0:def 3;
then A26:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))
by A9, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))))
by A11, XBOOLE_0:def 3;
then A27:
s1 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))) . d2
by A10, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))) . d2
by A26, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> (0. R))) . d2
by A21, FUNCT_4:12
.=
(d2 .--> (0. R)) . d2
by A25, FUNCT_4:14
.=
0. R
by FUNCOP_1:87
;
A28:
il <> d2
by Th7;
then A29:
not
il in dom (d2 .--> (0. R))
by A24, 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. R)))
by A23, XBOOLE_0:def 3;
then A30:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))
by A9, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))))
by A11, XBOOLE_0:def 3;
then A31:
s1 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))) . il
by A10, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R)))) . il
by A30, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> (0. R))) . il
by A17, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A29, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
X:
dom p c= the
carrier of
(SCM R)
by RELAT_1:def 18;
dom (Comput ((ProgramPart s1),s1,1)) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A32:
dom ((Comput ((ProgramPart s1),s1,1)) | (dom p)) = dom p
by X, RELAT_1:91;
consider e being
Element of
R such that A33:
e <> 0. R
by A1, STRUCT_0:def 19;
DataPart p c= p
by RELAT_1:88;
then A34:
dom (DataPart p) c= dom p
by RELAT_1:25;
set p2 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))));
consider s2 being
State of
(SCM R) such that A35:
p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))) 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. R))) +* (Start-At (il,(SCM R)))) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))) \/ (dom (Start-At (il,(SCM R))))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))) \/ {(IC (SCM R))}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> (0. R)))) \/ {(IC (SCM R))}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> (0. R)))) \/ {(IC (SCM R))}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC (SCM R))}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC (SCM R))})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A3, Lm1
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A6, Lm1
.=
{}
by A8, Lm1
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At (il,(SCM R))))
by FUNCT_4:33;
hence
p c= s1
by A10, 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 .--> e)) +* (Start-At (il,(SCM R)))) =
(dom ((il .--> (d1 := d2)) +* (d2 .--> e))) \/ (dom (Start-At (il,(SCM R))))
by FUNCT_4:def 1
.=
(dom ((il .--> (d1 := d2)) +* (d2 .--> e))) \/ {(IC (SCM R))}
by FUNCOP_1:19
.=
((dom (il .--> (d1 := d2))) \/ (dom (d2 .--> e))) \/ {(IC (SCM R))}
by FUNCT_4:def 1
.=
({il} \/ (dom (d2 .--> e))) \/ {(IC (SCM R))}
by FUNCOP_1:19
.=
({il} \/ {d2}) \/ {(IC (SCM R))}
by FUNCOP_1:19
;
then (dom p) /\ (dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))) =
((dom p) /\ ({il} \/ {d2})) \/ ((dom p) /\ {(IC (SCM R))})
by XBOOLE_1:23
.=
((dom p) /\ ({il} \/ {d2})) \/ {}
by A3, Lm1
.=
((dom p) /\ {il}) \/ ((dom p) /\ {d2})
by XBOOLE_1:23
.=
((dom p) /\ {il}) \/ {}
by A6, Lm1
.=
{}
by A8, Lm1
;
then
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))
by XBOOLE_0:def 7;
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))
by FUNCT_4:33;
hence
p c= s2
by A35, 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)
A36:
dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))) = (dom ((il .--> (d1 := d2)) +* (d2 .--> e))) \/ (dom (Start-At (il,(SCM R))))
by FUNCT_4:def 1;
A37:
dom (d2 .--> e) = {d2}
by FUNCOP_1:19;
then A38:
not
il in dom (d2 .--> e)
by A28, TARSKI:def 1;
A39:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))))
by FUNCT_4:def 1;
A40:
IC (SCM R) in dom (Start-At (il,(SCM R)))
by A18, TARSKI:def 1;
then A41:
IC (SCM R) in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))
by A36, XBOOLE_0:def 3;
then
IC (SCM R) in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))))
by A39, XBOOLE_0:def 3;
then A42:
IC s2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))) . (IC (SCM R))
by A35, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))) . (IC (SCM R))
by A41, FUNCT_4:14
.=
(Start-At (il,(SCM R))) . (IC (SCM R))
by A40, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
X:
dom p c= the
carrier of
(SCM R)
by RELAT_1:def 18;
dom (Comput ((ProgramPart s2),s2,1)) = the
carrier of
(SCM R)
by PARTFUN1:def 4;
then A43:
dom ((Comput ((ProgramPart s2),s2,1)) | (dom p)) = dom p
by X, RELAT_1:91;
A44:
dom ((il .--> (d1 := d2)) +* (d2 .--> e)) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> e))
by FUNCT_4: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 .--> e))
by A44, XBOOLE_0:def 3;
then A45:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))
by A36, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))))
by A39, XBOOLE_0:def 3;
then A46:
s2 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))) . il
by A35, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))) . il
by A45, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> e)) . il
by A19, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A38, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A47:
d2 in dom (d2 .--> e)
by A37, TARSKI:def 1;
then
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> e))
by A44, XBOOLE_0:def 3;
then A48:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))
by A36, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))))
by A39, XBOOLE_0:def 3;
then A49:
s2 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R))))) . d2
by A35, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At (il,(SCM R)))) . d2
by A48, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> e)) . d2
by A22, FUNCT_4:12
.=
(d2 .--> e) . d2
by A47, FUNCT_4:14
.=
e
by FUNCOP_1:87
;
X:
(ProgramPart s2) /. il = s2 . il
by COMPOS_1:38;
A50:
(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
.=
e
by A42, A46, A49, X, SCMRING2:13
;
X:
(ProgramPart s1) /. il = s1 . il
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. R
by A15, A31, A27, X, SCMRING2:13
;
then
((Comput ((ProgramPart s1),s1,1)) | (dom p)) . d1 = 0. R
by A4, A34, A32, FUNCT_1:70;
hence
(Comput ((ProgramPart s1),s1,1)) | (dom p) <> (Comput ((ProgramPart s2),s2,1)) | (dom p)
by A4, A33, A34, A43, A50, FUNCT_1:70;
verum
end;
hence
contradiction
; verum