let p be non NAT -defined autonomic FinPartState of ; :: according to AMISTD_5:def 4 :: thesis: for b₁ being set holds
( not p c= b₁ or for b₂ being set holds
( not ProgramPart p c= b₂ or for b₃ being Element of NAT holds IC (Comput (b₂,b₁,b₃)) in proj1 (ProgramPart p) ) )
let s be State of SCM+FSA; :: thesis: ( not p c= s or for b₁ being set holds
( not ProgramPart p c= b₁ or for b₂ being Element of NAT holds IC (Comput (b₁,s,b₂)) in proj1 (ProgramPart p) ) )
assume A1: p c= s ; :: thesis: for b₁ being set holds
( not ProgramPart p c= b₁ or for b₂ being Element of NAT holds IC (Comput (b₁,s,b₂)) in proj1 (ProgramPart p) )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart p c= P or for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in proj1 (ProgramPart p) )
assume A2: ProgramPart p c= P ; :: thesis: for b₁ being Element of NAT holds IC (Comput (P,s,b₁)) in proj1 (ProgramPart p)
let i be Element of NAT ; :: thesis: IC (Comput (P,s,i)) in proj1 (ProgramPart p)
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
reconsider ll = IC (Comput (P,s,i)) as Element of NAT ;
set loc1 = ll + 1;
A3: ( IC (Comput (P,s,i)) in dom (ProgramPart p) iff IC (Comput (P,s,i)) in (dom p) /\ NAT ) by RELAT_1:90;
assume not IC (Comput (P,s,i)) in dom (ProgramPart p) ; :: thesis: contradiction
then A4: not IC (Comput (P,s,i)) in dom p by A3, XBOOLE_0:def 4;
set p2 = p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)));
set p1 = p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))));
A5: dom (p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) = (dom p) \/ (dom ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) by FUNCT_4:def 1;
A6: dom ((IC (Comput (P,s,i))) .--> (goto (ll + 1))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:19;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (goto (ll + 1))) by TARSKI:def 1;
A8: dom (p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) = (dom p) \/ (dom ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) by FUNCT_4:def 1;
then A9: IC (Comput (P,s,i)) in dom (p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) by A7, XBOOLE_0:def 3;
consider s2 being State of SCM+FSA such that
A10: p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1))) c= s2 by PBOOLE:156;
set Cs2i = Comput ((ProgramPart s2),s2,i);
consider s1 being State of SCM+FSA such that
A11: p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i))))) c= s1 by PBOOLE:156;
set Cs1i = Comput ((ProgramPart s1),s1,i);
A12: dom ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i))))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:19;
then A13: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i))))) by TARSKI:def 1;
then A14: IC (Comput (P,s,i)) in dom (p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) by A5, XBOOLE_0:def 3;
not p is autonomic

proof

A15: now

let x be set ; :: thesis: ( x in dom p implies p . x = s2 . x )
assume A16: x in dom p ; :: thesis: p . x = s2 . x
dom p misses dom ((IC (Comput (P,s,i))) .--> (goto (ll + 1))) by A4, A6, ZFMISC_1:56;
then A17: p . x = (p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) . x by A16, FUNCT_4:17;
x in dom (p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) by A8, A16, XBOOLE_0:def 3;
hence p . x = s2 . x by A10, A17, GRFUNC_1:8; :: thesis: verum

end;

((IC (Comput (P,s,i))) .--> (goto (ll + 1))) . (IC (Comput (P,s,i))) = goto (ll + 1) by FUNCOP_1:87;
then (p +* ((IC (Comput (P,s,i))) .--> (goto (ll + 1)))) . (IC (Comput (P,s,i))) = goto (ll + 1) by A7, FUNCT_4:14;
then s2 . (IC (Comput (P,s,i))) = goto (ll + 1) by A9, A10, GRFUNC_1:8;
then A18: (Comput ((ProgramPart s2),s2,i)) . (IC (Comput (P,s,i))) = goto (ll + 1) by AMI_1:54;
((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i))))) . (IC (Comput (P,s,i))) = goto (IC (Comput (P,s,i))) by FUNCOP_1:87;
then (p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) . (IC (Comput (P,s,i))) = goto (IC (Comput (P,s,i))) by A13, FUNCT_4:14;
then s1 . (IC (Comput (P,s,i))) = goto (IC (Comput (P,s,i))) by A14, A11, GRFUNC_1:8;
then A19: (Comput ((ProgramPart s1),s1,i)) . (IC (Comput (P,s,i))) = goto (IC (Comput (P,s,i))) by AMI_1:54;
take P1 = ProgramPart s1; :: according to EXTPRO_1:def 9 :: thesis: ex b₁ being set st
( ProgramPart p c= P1 & ProgramPart p c= b₁ & ex b₂, b₃ being set st
( p c= b₂ & p c= b₃ & not for b₄ being Element of NAT holds (Comput (P1,b₂,b₄)) | (proj1 (NPP p)) = (Comput (b₁,b₃,b₄)) | (proj1 (NPP p)) ) )
take P2 = ProgramPart s2; :: thesis: ( ProgramPart p c= P1 & ProgramPart p c= P2 & ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (NPP p)) = (Comput (P2,b₂,b₃)) | (proj1 (NPP p)) ) )

A20: now

let x be set ; :: thesis: ( x in dom p implies p . x = s1 . x )
assume A21: x in dom p ; :: thesis: p . x = s1 . x
dom p misses dom ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i))))) by A4, A12, ZFMISC_1:56;
then A22: p . x = (p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) . x by A21, FUNCT_4:17;
x in dom (p +* ((IC (Comput (P,s,i))) .--> (goto (IC (Comput (P,s,i)))))) by A5, A21, XBOOLE_0:def 3;
hence p . x = s1 . x by A11, A22, GRFUNC_1:8; :: thesis: verum

end;

dom s1 = the carrier of SCM+FSA by PARTFUN1:def 4;
then dom p c= dom s1 by RELAT_1:def 18;
then A23: p c= s1 by A20, GRFUNC_1:8;
hence A24: ProgramPart p c= P1 by RELAT_1:105; :: thesis: ( ProgramPart p c= P2 & ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (NPP p)) = (Comput (P2,b₂,b₃)) | (proj1 (NPP p)) ) )
dom s2 = the carrier of SCM+FSA by PARTFUN1:def 4;
then dom p c= dom s2 by RELAT_1:def 18;
then A25: p c= s2 by A15, GRFUNC_1:8;
hence A26: ProgramPart p c= P2 by RELAT_1:105; :: thesis: ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (NPP p)) = (Comput (P2,b₂,b₃)) | (proj1 (NPP p)) )
take s1 ; :: thesis: ex b₁ being set st
( p c= s1 & p c= b₁ & not for b₂ being Element of NAT holds (Comput (P1,s1,b₂)) | (proj1 (NPP p)) = (Comput (P2,b₁,b₂)) | (proj1 (NPP p)) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (NPP p)) = (Comput (P2,s2,b₁)) | (proj1 (NPP p)) )
thus p c= s1 by A23; :: thesis: ( p c= s2 & not for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (NPP p)) = (Comput (P2,s2,b₁)) | (proj1 (NPP p)) )
then A27: (Comput ((ProgramPart s1),s1,i)) | (dom (NPP p)) = (Comput (P,s,i)) | (dom (NPP p)) by A1, EXTPRO_1:def 9, A24, A2;
thus p c= s2 by A25; :: thesis: not for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (NPP p)) = (Comput (P2,s2,b₁)) | (proj1 (NPP p))
then A28: (Comput ((ProgramPart s1),s1,i)) | (dom (NPP p)) = (Comput ((ProgramPart s2),s2,i)) | (dom (NPP p)) by EXTPRO_1:def 9, A26, A2, A1, A27;
take k = i + 1; :: thesis: not (Comput (P1,s1,k)) | (proj1 (NPP p)) = (Comput (P2,s2,k)) | (proj1 (NPP p))
set Cs1k = Comput (P1,s1,k);
A29: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,i)) by AMI_1:123;
A30: Comput (P1,s1,k) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput ((ProgramPart s1),s1,i)))),(Comput ((ProgramPart s1),s1,i))) ;
A31: (ProgramPart s1) /. (IC (Comput ((ProgramPart s1),s1,i))) = (Comput ((ProgramPart s1),s1,i)) . (IC (Comput ((ProgramPart s1),s1,i))) by A29, COMPOS_1:38;
IC in dom p by AMISTD_5:6;
then A32: IC in dom (NPP p) by COMPOS_1:179;
then A33: (Comput (P,s,i)) . (IC ) = ((Comput (P,s,i)) | (dom (NPP p))) . (IC ) by FUNCT_1:72;
then (Comput ((ProgramPart s1),s1,i)) . (IC ) = IC (Comput (P,s,i)) by A27, FUNCT_1:72, A32;
then A34: (Comput (P1,s1,k)) . (IC ) = IC (Comput (P,s,i)) by A30, A19, A31, SCMFSA_2:95;
set Cs2k = Comput (P2,s2,k);
A35: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,i)) by AMI_1:123;
A36: Comput (P2,s2,k) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i)))),(Comput ((ProgramPart s2),s2,i))) ;
A37: (ProgramPart s2) /. (IC (Comput ((ProgramPart s2),s2,i))) = (Comput ((ProgramPart s2),s2,i)) . (IC (Comput ((ProgramPart s2),s2,i))) by A35, COMPOS_1:38;
(Comput ((ProgramPart s2),s2,i)) . (IC ) = IC (Comput (P,s,i)) by A27, A33, A28, FUNCT_1:72, A32;
then A38: (Comput (P2,s2,k)) . (IC ) = ll + 1 by A36, A18, A37, SCMFSA_2:95;
( ((Comput (P1,s1,k)) | (dom (NPP p))) . (IC ) = (Comput (P1,s1,k)) . (IC ) & ((Comput (P2,s2,k)) | (dom (NPP p))) . (IC ) = (Comput (P2,s2,k)) . (IC ) ) by FUNCT_1:72, A32;
hence (Comput (P1,s1,k)) | (dom (NPP p)) <> (Comput (P2,s2,k)) | (dom (NPP p)) by A34, A38; :: thesis: verum

end;

hence contradiction ; :: thesis: verum