let n be Element of NAT ; :: thesis: for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p)
let R be good Ring; :: thesis: for s being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p)
let s be State of (SCM R); :: thesis: ( not R is trivial implies for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p) )
assume A1: not R is trivial ; :: thesis: for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p)
set Csi = Comput (ProgramPart s),s,n;
let p be non NAT -defined autonomic FinPartState of ; :: thesis: ( p c= s implies IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p) )
assume A2: p c= s ; :: thesis: IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p)
set loc = IC (Comput (ProgramPart s),s,n);
consider ll being natural number such that
A3: IC (Comput (ProgramPart s),s,n) = il. (SCM R),ll by AMISTD_1:26;
set loc1 = il. (SCM R),(ll + 1);
A4: IC (Comput (ProgramPart s),s,n) <> il. (SCM R),(ll + 1)

proof

assume IC (Comput (ProgramPart s),s,n) = il. (SCM R),(ll + 1) ; :: thesis: contradiction
then ll + 0 = ll + 1 by A3, AMISTD_1:25;
hence contradiction ; :: thesis: verum

end;

set p2 = p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R));
A5: ( IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p) iff IC (Comput (ProgramPart s),s,n) in (dom p) /\ NAT ) by RELAT_1:90;
set p1 = p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R));
A7: dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R)) = {(IC (Comput (ProgramPart s),s,n))} by FUNCOP_1:19;
then A8: IC (Comput (ProgramPart s),s,n) in dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R)) by TARSKI:def 1;
assume not IC (Comput (ProgramPart s),s,n) in dom (ProgramPart p) ; :: thesis: contradiction
then A9: not IC (Comput (ProgramPart s),s,n) in dom p by A5, XBOOLE_0:def 4;
consider s2 being State of (SCM R) such that
A10: p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R)) c= s2 by PBOOLE:156;
set Cs2i = Comput (ProgramPart s2),s2,n;
consider s1 being State of (SCM R) such that
A11: p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R)) c= s1 by PBOOLE:156;
set Cs1i = Comput (ProgramPart s1),s1,n;
A12: dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R)) = {(IC (Comput (ProgramPart s),s,n))} by FUNCOP_1:19;
then A13: IC (Comput (ProgramPart s),s,n) in dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R)) by TARSKI:def 1;
A14: dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) = (dom p) \/ (dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) by FUNCT_4:def 1;
then A15: IC (Comput (ProgramPart s),s,n) in dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) by A13, XBOOLE_0:def 3;
A16: dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) = (dom p) \/ (dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) by FUNCT_4:def 1;
then A17: IC (Comput (ProgramPart s),s,n) in dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) by A8, XBOOLE_0:def 3;
not p is autonomic

proof

A18: now

let x be set ; :: thesis: ( x in dom p implies p . x = s2 . x )
assume A19: x in dom p ; :: thesis: p . x = s2 . x
dom p misses dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R)) by A9, A12, ZFMISC_1:56;
then A20: p . x = (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) . x by A19, FUNCT_4:17;
x in dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) by A14, A19, XBOOLE_0:def 3;
hence p . x = s2 . x by A10, A20, GRFUNC_1:8; :: thesis: verum

end;

((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R)) . (IC (Comput (ProgramPart s),s,n)) = goto (il. (SCM R),(ll + 1)),R by FUNCOP_1:87;
then (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (il. (SCM R),(ll + 1)),R))) . (IC (Comput (ProgramPart s),s,n)) = goto (il. (SCM R),(ll + 1)),R by A13, FUNCT_4:14;
then s2 . (IC (Comput (ProgramPart s),s,n)) = goto (il. (SCM R),(ll + 1)),R by A15, A10, GRFUNC_1:8;
then A21: (Comput (ProgramPart s2),s2,n) . (IC (Comput (ProgramPart s),s,n)) = goto (il. (SCM R),(ll + 1)),R by AMI_1:54;
((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R)) . (IC (Comput (ProgramPart s),s,n)) = goto (IC (Comput (ProgramPart s),s,n)),R by FUNCOP_1:87;
then (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) . (IC (Comput (ProgramPart s),s,n)) = goto (IC (Comput (ProgramPart s),s,n)),R by A8, FUNCT_4:14;
then s1 . (IC (Comput (ProgramPart s),s,n)) = goto (IC (Comput (ProgramPart s),s,n)),R by A17, A11, GRFUNC_1:8;
then A22: (Comput (ProgramPart s1),s1,n) . (IC (Comput (ProgramPart s),s,n)) = goto (IC (Comput (ProgramPart s),s,n)),R by AMI_1:54;
take s1 ; :: according to AMI_1:def 25 :: thesis: ex b₁ being set st
( p c= s1 & p c= b₁ & not for b₂ being Element of NAT holds (Comput (ProgramPart s1),s1,b₂) | (proj1 p) = (Comput (ProgramPart b₁),b₁,b₂) | (proj1 p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p) )

A23: now

let x be set ; :: thesis: ( x in dom p implies p . x = s1 . x )
assume A24: x in dom p ; :: thesis: p . x = s1 . x
dom p misses dom ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R)) by A9, A7, ZFMISC_1:56;
then A25: p . x = (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) . x by A24, FUNCT_4:17;
x in dom (p +* ((IC (Comput (ProgramPart s),s,n)) .--> (goto (IC (Comput (ProgramPart s),s,n)),R))) by A16, A24, XBOOLE_0:def 3;
hence p . x = s1 . x by A11, A25, GRFUNC_1:8; :: thesis: verum

end;

dom s1 = the carrier of (SCM R) by PARTFUN1:def 4;
then dom p c= dom s1 by RELAT_1:def 18;
hence A26: p c= s1 by A23, GRFUNC_1:8; :: thesis: ( p c= s2 & not for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p) )
then A27: (Comput (ProgramPart s1),s1,n) | (dom p) = (Comput (ProgramPart s),s,n) | (dom p) by A2, AMI_1:def 25;
dom s2 = the carrier of (SCM R) by PARTFUN1:def 4;
then dom p c= dom s2 by RELAT_1:def 18;
hence p c= s2 by A18, GRFUNC_1:8; :: thesis: not for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p)
then A28: (Comput (ProgramPart s1),s1,n) | (dom p) = (Comput (ProgramPart s2),s2,n) | (dom p) by A26, AMI_1:def 25;
take k = n + 1; :: thesis: not (Comput (ProgramPart s1),s1,k) | (proj1 p) = (Comput (ProgramPart s2),s2,k) | (proj1 p)
set Cs1k = Comput (ProgramPart s1),s1,k;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,n) by AMI_1:144;
A29: Comput (ProgramPart s1),s1,k = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,n) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) by T ;
Y: (ProgramPart (Comput (ProgramPart s1),s1,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s1),s1,n) . (IC (Comput (ProgramPart s),s,n)) by AMI_1:150;
A30: (Comput (ProgramPart s),s,n) . (IC (SCM R)) = ((Comput (ProgramPart s),s,n) | (dom p)) . (IC (SCM R)) by A1, Th25, FUNCT_1:72;
then (Comput (ProgramPart s1),s1,n) . (IC (SCM R)) = IC (Comput (ProgramPart s),s,n) by A1, A27, Th25, FUNCT_1:72;
then A31: (Comput (ProgramPart s1),s1,k) . (IC (SCM R)) = IC (Comput (ProgramPart s),s,n) by A29, A22, SCMRING2:17, Y;
set Cs2k = Comput (ProgramPart s2),s2,k;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,n) by AMI_1:144;
A32: Comput (ProgramPart s2),s2,k = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,n) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) by T ;
Y: (ProgramPart (Comput (ProgramPart s2),s2,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s2),s2,n) . (IC (Comput (ProgramPart s),s,n)) by AMI_1:150;
(Comput (ProgramPart s2),s2,n) . (IC (SCM R)) = IC (Comput (ProgramPart s),s,n) by A1, A27, A30, A28, Th25, FUNCT_1:72;
then A33: (Comput (ProgramPart s2),s2,k) . (IC (SCM R)) = il. (SCM R),(ll + 1) by A32, A21, SCMRING2:17, Y;
((Comput (ProgramPart s1),s1,k) | (dom p)) . (IC (SCM R)) = (Comput (ProgramPart s1),s1,k) . (IC (SCM R)) by A1, Th25, FUNCT_1:72;
hence (Comput (ProgramPart s1),s1,k) | (dom p) <> (Comput (ProgramPart s2),s2,k) | (dom p) by A1, A4, A31, A33, Th25, FUNCT_1:72; :: thesis: verum

end;

hence contradiction ; :: thesis: verum