let n be Element of NAT ; :: thesis: for R being good Ring
for s being State of st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Computation s,n) in dom (ProgramPart p)
let R be good Ring; :: thesis: for s being State of st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Computation s,n) in dom (ProgramPart p)
let s be State of ; :: thesis: ( not R is trivial implies for p being non NAT -defined autonomic FinPartState of st p c= s holds
IC (Computation 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 (Computation s,n) in dom (ProgramPart p)
set Csi = Computation s,n;
let p be non NAT -defined autonomic FinPartState of ; :: thesis: ( p c= s implies IC (Computation s,n) in dom (ProgramPart p) )
assume A2: p c= s ; :: thesis: IC (Computation s,n) in dom (ProgramPart p)
set loc = IC (Computation s,n);
consider ll being natural number such that
A3: IC (Computation s,n) = il. (SCM R),ll by AMISTD_1:26;
set loc1 = il. (SCM R),(ll + 1);
A4: IC (Computation s,n) <> il. (SCM R),(ll + 1)
proof
assume IC (Computation 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 (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))));
A5: ( IC (Computation s,n) in dom (ProgramPart p) iff IC (Computation s,n) in (dom p) /\ NAT ) by RELAT_1:90;
set p1 = p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))));
A6: IC (Computation s,n) in NAT by AMI_1:def 4;
A7: dom ((IC (Computation s,n)) .--> (goto (IC (Computation s,n)))) = {(IC (Computation s,n))} by FUNCOP_1:19;
then A8: IC (Computation s,n) in dom ((IC (Computation s,n)) .--> (goto (IC (Computation s,n)))) by TARSKI:def 1;
assume not IC (Computation s,n) in dom (ProgramPart p) ; :: thesis: contradiction
then A9: not IC (Computation s,n) in dom p by A6, A5, XBOOLE_0:def 4;
consider s2 being State of such that
A10: p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1)))) c= s2 by CARD_3:97;
set Cs2i = Computation s2,n;
consider s1 being State of such that
A11: p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n)))) c= s1 by CARD_3:97;
set Cs1i = Computation s1,n;
A12: dom ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1)))) = {(IC (Computation s,n))} by FUNCOP_1:19;
then A13: IC (Computation s,n) in dom ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1)))) by TARSKI:def 1;
A14: dom (p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) = (dom p) \/ (dom ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) by FUNCT_4:def 1;
then A15: IC (Computation s,n) in dom (p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) by A13, XBOOLE_0:def 3;
A16: dom (p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) = (dom p) \/ (dom ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) by FUNCT_4:def 1;
then A17: IC (Computation s,n) in dom (p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) 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 (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1)))) by A9, A12, ZFMISC_1:56;
then A20: p . x = (p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) . x by A19, FUNCT_4:17;
x in dom (p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) by A14, A19, XBOOLE_0:def 3;
hence p . x = s2 . x by A10, A20, GRFUNC_1:8; :: thesis: verum
end;
((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1)))) . (IC (Computation s,n)) = goto (il. (SCM R),(ll + 1)) by FUNCOP_1:87;
then (p +* ((IC (Computation s,n)) .--> (goto (il. (SCM R),(ll + 1))))) . (IC (Computation s,n)) = goto (il. (SCM R),(ll + 1)) by A13, FUNCT_4:14;
then s2 . (IC (Computation s,n)) = goto (il. (SCM R),(ll + 1)) by A15, A10, GRFUNC_1:8;
then A21: (Computation s2,n) . (IC (Computation s,n)) = goto (il. (SCM R),(ll + 1)) by AMI_1:54;
((IC (Computation s,n)) .--> (goto (IC (Computation s,n)))) . (IC (Computation s,n)) = goto (IC (Computation s,n)) by FUNCOP_1:87;
then (p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) . (IC (Computation s,n)) = goto (IC (Computation s,n)) by A8, FUNCT_4:14;
then s1 . (IC (Computation s,n)) = goto (IC (Computation s,n)) by A17, A11, GRFUNC_1:8;
then A22: (Computation s1,n) . (IC (Computation s,n)) = goto (IC (Computation s,n)) by AMI_1:54;
take s1 ; :: according to AMI_1:def 25 :: thesis: ex b1 being Element of product the Object-Kind of (SCM R) 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) )
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 (Computation s,n)) .--> (goto (IC (Computation s,n)))) by A9, A7, ZFMISC_1:56;
then A25: p . x = (p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) . x by A24, FUNCT_4:17;
x in dom (p +* ((IC (Computation s,n)) .--> (goto (IC (Computation s,n))))) 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 AMI_1:79;
then dom p c= dom s1 by AMI_1:80;
hence A26: p c= s1 by A23, GRFUNC_1:8; :: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
then A27: (Computation s1,n) | (dom p) = (Computation s,n) | (dom p) by A2, AMI_1:def 25;
dom s2 = the carrier of (SCM R) by AMI_1:79;
then dom p c= dom s2 by AMI_1:80;
hence p c= s2 by A18, GRFUNC_1:8; :: thesis: not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p)
then A28: (Computation s1,n) | (dom p) = (Computation s2,n) | (dom p) by A26, AMI_1:def 25;
take k = n + 1; :: thesis: not (Computation s1,k) | (dom p) = (Computation s2,k) | (dom p)
set Cs1k = Computation s1,k;
A29: Computation s1,k = Following (Computation s1,n) by AMI_1:14
.= Exec (CurInstr (Computation s1,n)),(Computation s1,n) ;
A30: (Computation s,n) . (IC (SCM R)) = ((Computation s,n) | (dom p)) . (IC (SCM R)) by A1, Th25, FUNCT_1:72;
then (Computation s1,n) . (IC (SCM R)) = IC (Computation s,n) by A1, A27, Th25, FUNCT_1:72;
then A31: (Computation s1,k) . (IC (SCM R)) = IC (Computation s,n) by A29, A22, SCMRING2:17;
set Cs2k = Computation s2,k;
A32: Computation s2,k = Following (Computation s2,n) by AMI_1:14
.= Exec (CurInstr (Computation s2,n)),(Computation s2,n) ;
(Computation s2,n) . (IC (SCM R)) = IC (Computation s,n) by A1, A27, A30, A28, Th25, FUNCT_1:72;
then A33: (Computation s2,k) . (IC (SCM R)) = il. (SCM R),(ll + 1) by A32, A21, SCMRING2:17;
((Computation s1,k) | (dom p)) . (IC (SCM R)) = (Computation s1,k) . (IC (SCM R)) by A1, Th25, FUNCT_1:72;
hence (Computation s1,k) | (dom p) <> (Computation s2,k) | (dom p) by A1, A4, A31, A33, Th25, FUNCT_1:72; :: thesis: verum
end;
hence contradiction ; :: thesis: verum