let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s being State of SCM st p c= s holds
for i being Element of NAT holds IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p)
let s be State of SCM ; :: thesis: ( p c= s implies for i being Element of NAT holds IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p) )
assume A1: p c= s ; :: thesis: for i being Element of NAT holds IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p)
let i be Element of NAT ; :: thesis: IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p)
set Csi = Comput (ProgramPart s),s,i;
set loc = IC (Comput (ProgramPart s),s,i);
reconsider ll = IC (Comput (ProgramPart s),s,i) as Element of NAT ;
set loc1 = ll + 1;
A3: ( IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p) iff IC (Comput (ProgramPart s),s,i) in (dom p) /\ NAT ) by RELAT_1:90;
assume not IC (Comput (ProgramPart s),s,i) in dom (ProgramPart p) ; :: thesis: contradiction
then A4: not IC (Comput (ProgramPart s),s,i) in dom p by A3, XBOOLE_0:def 4;
set p2 = p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)));
set p1 = p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i))));
A5: dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i))))) = (dom p) \/ (dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i))))) by FUNCT_4:def 1;
A6: dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1))) = {(IC (Comput (ProgramPart s),s,i))} by FUNCOP_1:19;
then A7: IC (Comput (ProgramPart s),s,i) in dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1))) by TARSKI:def 1;
A8: dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)))) = (dom p) \/ (dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)))) by FUNCT_4:def 1;
then A9: IC (Comput (ProgramPart s),s,i) in dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)))) by A7, XBOOLE_0:def 3;
consider s2 being State of SCM such that
A10: p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1))) c= s2 by PBOOLE:156;
set Cs2i = Comput (ProgramPart s2),s2,i;
consider s1 being State of SCM such that
A11: p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i)))) c= s1 by PBOOLE:156;
set Cs1i = Comput (ProgramPart s1),s1,i;
A12: dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i)))) = {(IC (Comput (ProgramPart s),s,i))} by FUNCOP_1:19;
then A13: IC (Comput (ProgramPart s),s,i) in dom ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i)))) by TARSKI:def 1;
then A14: IC (Comput (ProgramPart s),s,i) in dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),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 (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1))) by A4, A6, ZFMISC_1:56;
then A17: p . x = (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)))) . x by A16, FUNCT_4:17;
x in dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-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 (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1))) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (ll + 1) by FUNCOP_1:87;
then (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (ll + 1)))) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (ll + 1) by A7, FUNCT_4:14;
then s2 . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (ll + 1) by A9, A10, GRFUNC_1:8;
then A18: (Comput (ProgramPart s2),s2,i) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (ll + 1) by AMI_1:54;
((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i)))) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (IC (Comput (ProgramPart s),s,i)) by FUNCOP_1:87;
then (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i))))) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (IC (Comput (ProgramPart s),s,i)) by A13, FUNCT_4:14;
then s1 . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (IC (Comput (ProgramPart s),s,i)) by A14, A11, GRFUNC_1:8;
then A19: (Comput (ProgramPart s1),s1,i) . (IC (Comput (ProgramPart s),s,i)) = SCM-goto (IC (Comput (ProgramPart s),s,i)) 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 K98() 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 K98() holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 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 (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i)))) by A4, A12, ZFMISC_1:56;
then A22: p . x = (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),s,i))))) . x by A21, FUNCT_4:17;
x in dom (p +* ((IC (Comput (ProgramPart s),s,i)) .--> (SCM-goto (IC (Comput (ProgramPart s),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 by PARTFUN1:def 4;
then dom p c= dom s1 by RELAT_1:def 18;
hence A23: p c= s1 by A20, GRFUNC_1:8; :: thesis: ( p c= s2 & not for b₁ being Element of K98() holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p) )
then A24: (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s),s,i) | (dom p) by A1, AMI_1:def 25;
dom s2 = the carrier of SCM by PARTFUN1:def 4;
then dom p c= dom s2 by RELAT_1:def 18;
hence p c= s2 by A15, GRFUNC_1:8; :: thesis: not for b₁ being Element of K98() holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p)
then A25: (Comput (ProgramPart s1),s1,i) | (dom p) = (Comput (ProgramPart s2),s2,i) | (dom p) by A23, AMI_1:def 25;
take k = i + 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,i) by AMI_1:144;
Y: (ProgramPart (Comput (ProgramPart s1),s1,i)) /. (IC (Comput (ProgramPart s1),s1,i)) = (Comput (ProgramPart s1),s1,i) . (IC (Comput (ProgramPart s1),s1,i)) by AMI_1:150;
A26: Comput (ProgramPart s1),s1,k = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,i) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) by T ;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,i) by AMI_1:144;
A27: (Comput (ProgramPart s),s,i) . (IC SCM ) = ((Comput (ProgramPart s),s,i) | (dom p)) . (IC SCM ) by Th84, FUNCT_1:72;
then (Comput (ProgramPart s1),s1,i) . (IC SCM ) = IC (Comput (ProgramPart s),s,i) by A24, Th84, FUNCT_1:72;
then A28: (Comput (ProgramPart s1),s1,k) . (IC SCM ) = IC (Comput (ProgramPart s),s,i) by A26, A19, AMI_3:13, Y;
set Cs2k = Comput (ProgramPart s2),s2,k;
A29: Comput (ProgramPart s2),s2,k = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,i) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) by T ;
Y: (ProgramPart (Comput (ProgramPart s2),s2,i)) /. (IC (Comput (ProgramPart s2),s2,i)) = (Comput (ProgramPart s2),s2,i) . (IC (Comput (ProgramPart s2),s2,i)) by AMI_1:150;
(Comput (ProgramPart s2),s2,i) . (IC SCM ) = IC (Comput (ProgramPart s),s,i) by A24, A27, A25, Th84, FUNCT_1:72;
then A30: (Comput (ProgramPart s2),s2,k) . (IC SCM ) = ll + 1 by A29, A18, AMI_3:13, Y;
( ((Comput (ProgramPart s1),s1,k) | (dom p)) . (IC SCM ) = (Comput (ProgramPart s1),s1,k) . (IC SCM ) & ((Comput (ProgramPart s2),s2,k) | (dom p)) . (IC SCM ) = (Comput (ProgramPart s2),s2,k) . (IC SCM ) ) by Th84, FUNCT_1:72;
hence not (Comput (ProgramPart s1),s1,k) | (proj1 p) = (Comput (ProgramPart s2),s2,k) | (proj1 p) by A28, A30; :: thesis: verum

end;

hence contradiction ; :: thesis: verum