let p be non NAT -defined autonomic FinPartState of ; :: according to AMISTD_5:def 4 :: thesis: for b1 being set holds
( not p c= b1 or for b2 being set holds
( not ProgramPart p c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in proj1 (ProgramPart p) ) )
let s be State of (SCM R); :: thesis: ( not p c= s or for b1 being set holds
( not ProgramPart p c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 (ProgramPart p) ) )
assume A1: p c= s ; :: thesis: for b1 being set holds
( not ProgramPart p c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 (ProgramPart p) )
let P be the Instructions of (SCM R) -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart p c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 (ProgramPart p) )
assume A2: ProgramPart p c= P ; :: thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 (ProgramPart p)
let n be Element of NAT ; :: thesis: IC (Comput (P,s,n)) in proj1 (ProgramPart p)
set Csi = Comput (P,s,n);
set loc = IC (Comput (P,s,n));
consider ll being natural number such that
A3: IC (Comput (P,s,n)) = ll ;
set loc1 = ll + 1;
A4: IC (Comput (P,s,n)) <> ll + 1 by A3;
set p2 = p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)));
A5: ( IC (Comput (P,s,n)) in dom (ProgramPart p) iff IC (Comput (P,s,n)) in (dom p) /\ NAT ) by RELAT_1:90;
set p1 = p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)));
A6: dom ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R))) = {(IC (Comput (P,s,n)))} by FUNCOP_1:19;
then A7: IC (Comput (P,s,n)) in dom ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R))) by TARSKI:def 1;
assume not IC (Comput (P,s,n)) in dom (ProgramPart p) ; :: thesis: contradiction
then A8: not IC (Comput (P,s,n)) in dom p by A5, XBOOLE_0:def 4;
consider s2 being State of (SCM R) such that
A9: p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R))) c= s2 by PBOOLE:156;
set Cs2i = Comput ((ProgramPart s2),s2,n);
consider s1 being State of (SCM R) such that
A10: p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R))) c= s1 by PBOOLE:156;
set Cs1i = Comput ((ProgramPart s1),s1,n);
A11: dom ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R))) = {(IC (Comput (P,s,n)))} by FUNCOP_1:19;
then A12: IC (Comput (P,s,n)) in dom ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R))) by TARSKI:def 1;
A13: dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) = (dom p) \/ (dom ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) by FUNCT_4:def 1;
then A14: IC (Comput (P,s,n)) in dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) by A12, XBOOLE_0:def 3;
A15: dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) = (dom p) \/ (dom ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) by FUNCT_4:def 1;
then A16: IC (Comput (P,s,n)) in dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) by A7, XBOOLE_0:def 3;
not p is autonomic
proof
A17: now
let x be set ; :: thesis: ( x in dom p implies p . x = s2 . x )
assume A18: x in dom p ; :: thesis: p . x = s2 . x
dom p misses dom ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R))) by A8, A11, ZFMISC_1:56;
then A19: p . x = (p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) . x by A18, FUNCT_4:17;
x in dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) by A13, A18, XBOOLE_0:def 3;
hence p . x = s2 . x by A9, A19, GRFUNC_1:8; :: thesis: verum
end;
((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R))) . (IC (Comput (P,s,n))) = goto ((ll + 1),R) by FUNCOP_1:87;
then (p +* ((IC (Comput (P,s,n))) .--> (goto ((ll + 1),R)))) . (IC (Comput (P,s,n))) = goto ((ll + 1),R) by A12, FUNCT_4:14;
then s2 . (IC (Comput (P,s,n))) = goto ((ll + 1),R) by A14, A9, GRFUNC_1:8;
then A20: (Comput ((ProgramPart s2),s2,n)) . (IC (Comput (P,s,n))) = goto ((ll + 1),R) by AMI_1:54;
((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R))) . (IC (Comput (P,s,n))) = goto ((IC (Comput (P,s,n))),R) by FUNCOP_1:87;
then (p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) . (IC (Comput (P,s,n))) = goto ((IC (Comput (P,s,n))),R) by A7, FUNCT_4:14;
then s1 . (IC (Comput (P,s,n))) = goto ((IC (Comput (P,s,n))),R) by A16, A10, GRFUNC_1:8;
then A21: (Comput ((ProgramPart s1),s1,n)) . (IC (Comput (P,s,n))) = goto ((IC (Comput (P,s,n))),R) by AMI_1:54;
take P1 = ProgramPart s1; :: according to EXTPRO_1:def 9 :: thesis: ex b1 being set st
( ProgramPart p c= P1 & ProgramPart p c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 (NPP p)) = (Comput (b1,b3,b4)) | (proj1 (NPP p)) ) )
take P2 = ProgramPart s2; :: thesis: ( ProgramPart p c= P1 & ProgramPart p c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) ) )
A22: now
let x be set ; :: thesis: ( x in dom p implies p . x = s1 . x )
assume A23: x in dom p ; :: thesis: p . x = s1 . x
dom p misses dom ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R))) by A8, A6, ZFMISC_1:56;
then A24: p . x = (p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) . x by A23, FUNCT_4:17;
x in dom (p +* ((IC (Comput (P,s,n))) .--> (goto ((IC (Comput (P,s,n))),R)))) by A15, A23, XBOOLE_0:def 3;
hence p . x = s1 . x by A10, A24, 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;
then A25: p c= s1 by A22, GRFUNC_1:8;
hence A26: ProgramPart p c= P1 by RELAT_1:105; :: thesis: ( ProgramPart p c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) ) )
dom s2 = the carrier of (SCM R) by PARTFUN1:def 4;
then dom p c= dom s2 by RELAT_1:def 18;
then A27: p c= s2 by A17, GRFUNC_1:8;
hence A28: ProgramPart p c= P2 by RELAT_1:105; :: thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) )
take s1 ; :: thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s1,b2)) | (proj1 (NPP p)) = (Comput (P2,b1,b2)) | (proj1 (NPP p)) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p)) )
thus p c= s1 by A25; :: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p)) )
A29: (Comput ((ProgramPart s1),s1,n)) | (dom (NPP p)) = (Comput (P,s,n)) | (dom (NPP p)) by A1, EXTPRO_1:def 9, A2, A26, A25;
thus p c= s2 by A27; :: thesis: not for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (NPP p)) = (Comput (P2,s2,b1)) | (proj1 (NPP p))
A30: (Comput ((ProgramPart s1),s1,n)) | (dom (NPP p)) = (Comput ((ProgramPart s2),s2,n)) | (dom (NPP p)) by A1, A29, EXTPRO_1:def 9, A2, A28, A27;
take k = n + 1; :: thesis: not (Comput (P1,s1,k)) | (proj1 (NPP p)) = (Comput (P2,s2,k)) | (proj1 (NPP p))
set Cs1k = Comput ((ProgramPart s1),s1,k);
A31: Comput ((ProgramPart s1),s1,k) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n)))),(Comput ((ProgramPart s1),s1,n))) by AMI_1:123 ;
A32: (ProgramPart (Comput ((ProgramPart s1),s1,n))) /. (IC (Comput (P,s,n))) = (Comput ((ProgramPart s1),s1,n)) . (IC (Comput (P,s,n))) by COMPOS_1:38;
A33: IC in dom p by AMISTD_5:6;
A34: (Comput (P,s,n)) . (IC ) = ((Comput (P,s,n)) | (dom (NPP p))) . (IC ) by FUNCT_1:72, A33, COMPOS_1:179;
then (Comput ((ProgramPart s1),s1,n)) . (IC ) = IC (Comput (P,s,n)) by A29, FUNCT_1:72, A33, COMPOS_1:179;
then A35: (Comput ((ProgramPart s1),s1,k)) . (IC ) = IC (Comput (P,s,n)) by A31, A21, A32, SCMRING2:17;
set Cs2k = Comput ((ProgramPart s2),s2,k);
A36: Comput ((ProgramPart s2),s2,k) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,n))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n)))),(Comput ((ProgramPart s2),s2,n))) by AMI_1:123 ;
A37: (ProgramPart (Comput ((ProgramPart s2),s2,n))) /. (IC (Comput (P,s,n))) = (Comput ((ProgramPart s2),s2,n)) . (IC (Comput (P,s,n))) by COMPOS_1:38;
A38: (Comput ((ProgramPart s2),s2,n)) . (IC ) = IC (Comput (P,s,n)) by A29, A34, A30, FUNCT_1:72, A33, COMPOS_1:179;
then (Comput ((ProgramPart s2),s2,k)) . (IC ) = ll + 1 by A36, A20, A37, SCMRING2:17;
( ((Comput ((ProgramPart s1),s1,k)) | (dom (NPP p))) . (IC ) = (Comput ((ProgramPart s1),s1,k)) . (IC ) & ((Comput ((ProgramPart s2),s2,k)) | (dom (NPP p))) . (IC ) = (Comput ((ProgramPart s2),s2,k)) . (IC ) ) by FUNCT_1:72, A33, COMPOS_1:179;
hence not (Comput (P1,s1,k)) | (proj1 (NPP p)) = (Comput (P2,s2,k)) | (proj1 (NPP p)) by A4, A35, A38, A36, A20, A37, SCMRING2:17; :: thesis: verum
end;
hence contradiction ; :: thesis: verum