let p be autonomic non programmed FinPartState of SCM+FSA ; :: thesis: for s being State of SCM+FSA st p c= s holds
for i being Element of NAT holds IC (Computation s,i) in dom (ProgramPart p)
let s be State of SCM+FSA ; :: thesis: ( p c= s implies for i being Element of NAT holds IC (Computation s,i) in dom (ProgramPart p) )
assume A1: p c= s ; :: thesis: for i being Element of NAT holds IC (Computation s,i) in dom (ProgramPart p)
let i be Element of NAT ; :: thesis: IC (Computation s,i) in dom (ProgramPart p)
set Csi = Computation s,i;
set loc = IC (Computation s,i);
reconsider ll = IC (Computation s,i) as Element of NAT by ORDINAL1:def 13;
set loc1 = insloc (ll + 1);
assume A3: not IC (Computation s,i) in dom (ProgramPart p) ; :: thesis: contradiction
A4: IC (Computation s,i) in NAT by AMI_1:def 4;
( IC (Computation s,i) in dom (ProgramPart p) iff IC (Computation s,i) in (dom p) /\ NAT ) by FUNCT_1:68;
then A5: not IC (Computation s,i) in dom p by A3, A4, XBOOLE_0:def 4;
set p1 = p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))));
set p2 = p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))));
A6: ( dom (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) = (dom p) \/ (dom ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) & dom (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) = (dom p) \/ (dom ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) ) by FUNCT_4:def 1;
A7: ( dom ((IC (Computation s,i)) .--> (goto (IC (Computation s,i)))) = {(IC (Computation s,i))} & dom ((IC (Computation s,i)) .--> (goto (insloc (ll + 1)))) = {(IC (Computation s,i))} ) by FUNCOP_1:19;
then A8: ( IC (Computation s,i) in dom ((IC (Computation s,i)) .--> (goto (IC (Computation s,i)))) & IC (Computation s,i) in dom ((IC (Computation s,i)) .--> (goto (insloc (ll + 1)))) ) by TARSKI:def 1;
then A9: ( IC (Computation s,i) in dom (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) & IC (Computation s,i) in dom (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) ) by A6, XBOOLE_0:def 3;
consider s1 being State of SCM+FSA such that
A10: p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i)))) c= s1 by CARD_3:97;
consider s2 being State of SCM+FSA such that
A11: p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1)))) c= s2 by CARD_3:97;
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
not p is autonomic

proof

take s1 ; :: according to AMI_1:def 25 :: thesis: ex b₁ being Element of K260(the Object-Kind of SCM+FSA ) st
( p c= s1 & p c= b₁ & not for b₂ being Element of NAT holds (Computation s1,b₂) | (dom p) = (Computation b₁,b₂) | (dom p) )
take s2 ; :: thesis: ( p c= s1 & p c= s2 & not for b₁ being Element of NAT holds (Computation s1,b₁) | (dom p) = (Computation s2,b₁) | (dom p) )
( dom s1 = the carrier of SCM+FSA & dom s2 = the carrier of SCM+FSA ) by AMI_1:79;
then A12: ( dom p c= dom s1 & dom p c= dom s2 ) by AMI_1:80;

now

let x be set ; :: thesis: ( x in dom p implies p . x = s1 . x )
assume A13: x in dom p ; :: thesis: p . x = s1 . x
then ( dom p misses dom ((IC (Computation s,i)) .--> (goto (IC (Computation s,i)))) & x in dom (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) ) by A5, A6, A7, XBOOLE_0:def 3, ZFMISC_1:56;
then ( p . x = (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) . x & (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) . x = s1 . x ) by A10, A13, FUNCT_4:17, GRFUNC_1:8;
hence p . x = s1 . x ; :: thesis: verum

end;

hence A14: p c= s1 by A12, GRFUNC_1:8; :: thesis: ( p c= s2 & not for b₁ being Element of NAT holds (Computation s1,b₁) | (dom p) = (Computation s2,b₁) | (dom p) )

now

let x be set ; :: thesis: ( x in dom p implies p . x = s2 . x )
assume A15: x in dom p ; :: thesis: p . x = s2 . x
then ( dom p misses dom ((IC (Computation s,i)) .--> (goto (insloc (ll + 1)))) & x in dom (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) ) by A5, A6, A7, XBOOLE_0:def 3, ZFMISC_1:56;
then ( p . x = (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) . x & (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) . x = s2 . x ) by A11, A15, FUNCT_4:17, GRFUNC_1:8;
hence p . x = s2 . x ; :: thesis: verum

end;

hence A16: p c= s2 by A12, GRFUNC_1:8; :: thesis: not for b₁ being Element of NAT holds (Computation s1,b₁) | (dom p) = (Computation s2,b₁) | (dom p)
( ((IC (Computation s,i)) .--> (goto (IC (Computation s,i)))) . (IC (Computation s,i)) = goto (IC (Computation s,i)) & ((IC (Computation s,i)) .--> (goto (insloc (ll + 1)))) . (IC (Computation s,i)) = goto (insloc (ll + 1)) ) by FUNCOP_1:87;
then ( (p +* ((IC (Computation s,i)) .--> (goto (IC (Computation s,i))))) . (IC (Computation s,i)) = goto (IC (Computation s,i)) & (p +* ((IC (Computation s,i)) .--> (goto (insloc (ll + 1))))) . (IC (Computation s,i)) = goto (insloc (ll + 1)) ) by A8, FUNCT_4:14;
then A17: ( s1 . (IC (Computation s,i)) = goto (IC (Computation s,i)) & s2 . (IC (Computation s,i)) = goto (insloc (ll + 1)) ) by A9, A10, A11, GRFUNC_1:8;
take k = i + 1; :: thesis: not (Computation s1,k) | (dom p) = (Computation s2,k) | (dom p)
set Cs1k = Computation s1,k;
set Cs2k = Computation s2,k;
A18: Computation s1,k = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s1,i)),(Computation s1,i) ;
A19: Computation s2,k = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
A20: ( (Computation s1,i) . (IC (Computation s,i)) = goto (IC (Computation s,i)) & (Computation s2,i) . (IC (Computation s,i)) = goto (insloc (ll + 1)) ) by A17, AMI_1:54;
A21: (Computation s1,i) | (dom p) = (Computation s,i) | (dom p) by A1, A14, AMI_1:def 25;
A22: ( (Computation s1,i) . (IC SCM+FSA ) = ((Computation s1,i) | (dom p)) . (IC SCM+FSA ) & (Computation s,i) . (IC SCM+FSA ) = ((Computation s,i) | (dom p)) . (IC SCM+FSA ) ) by Th15, FUNCT_1:72;
(Computation s1,i) | (dom p) = (Computation s2,i) | (dom p) by A14, A16, AMI_1:def 25;
then ( (Computation s1,i) . (IC SCM+FSA ) = IC (Computation s,i) & (Computation s2,i) . (IC SCM+FSA ) = IC (Computation s,i) ) by A21, A22, Th15, FUNCT_1:72;
then A23: ( (Computation s1,k) . (IC SCM+FSA ) = IC (Computation s,i) & (Computation s2,k) . (IC SCM+FSA ) = insloc (ll + 1) ) by A18, A19, A20, SCMFSA_2:95;
( ((Computation s1,k) | (dom p)) . (IC SCM+FSA ) = (Computation s1,k) . (IC SCM+FSA ) & ((Computation s2,k) | (dom p)) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) ) by Th15, FUNCT_1:72;
hence (Computation s1,k) | (dom p) <> (Computation s2,k) | (dom p) by A23; :: thesis: verum

end;

hence contradiction ; :: thesis: verum