let p be autonomic FinPartState of SCMPDS ; :: thesis: ( IC SCMPDS in dom p implies IC p in dom p )
assume A1: IC SCMPDS in dom p ; :: thesis: IC p in dom p
set il = IC p;
set p1 = p +* ((IC p) .--> (goto 0 ));
set p2 = p +* ((IC p) .--> (goto 1));
consider s1 being State of SCMPDS such that
A2: p +* ((IC p) .--> (goto 0 )) c= s1 by PBOOLE:156;
consider s2 being State of SCMPDS such that
A3: p +* ((IC p) .--> (goto 1)) c= s2 by PBOOLE:156;
assume A4: not IC p in dom p ; :: thesis: contradiction
not p is autonomic

proof

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 NAT 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 NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p) )
A5: dom ((IC p) .--> (goto 1)) = {(IC p)} by FUNCOP_1:19;
then A6: IC p in dom ((IC p) .--> (goto 1)) by TARSKI:def 1;
A7: dom ((IC p) .--> (goto 0 )) = {(IC p)} by FUNCOP_1:19;
then A8: IC p in dom ((IC p) .--> (goto 0 )) by TARSKI:def 1;
A9: dom p misses {(IC p)} by A4, ZFMISC_1:56;
then A10: p c= p +* ((IC p) .--> (goto 0 )) by A7, FUNCT_4:33;
A11: p c= p +* ((IC p) .--> (goto 1)) by A5, A9, FUNCT_4:33;
hence ( p c= s1 & p c= s2 ) by A2, A3, A10, XBOOLE_1:1; :: thesis: not for b₁ being Element of NAT holds (Comput (ProgramPart s1),s1,b₁) | (proj1 p) = (Comput (ProgramPart s2),s2,b₁) | (proj1 p)
dom (p +* ((IC p) .--> (goto 1))) = (dom p) \/ (dom ((IC p) .--> (goto 1))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto 1))) by A6, XBOOLE_0:def 3;
then X: s2 . (IC p) = (p +* ((IC p) .--> (goto 1))) . (IC p) by A3, GRFUNC_1:8
.= ((IC p) .--> (goto 1)) . (IC p) by A6, FUNCT_4:14
.= goto 1 by FUNCOP_1:87 ;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by AMI_1:150;
x: p c= s2 by A3, A11, XBOOLE_1:1;
then A12: (Following (ProgramPart s2),s2) . (IC SCMPDS ) = (Exec (goto 1),s2) . (IC SCMPDS ) by A1, GRFUNC_1:8, X, Y
.= ICplusConst s2,1 by SCMPDS_2:66 ;
take 1 ; :: thesis: not (Comput (ProgramPart s1),s1,1) | (proj1 p) = (Comput (ProgramPart s2),s2,1) | (proj1 p)
assume A13: (Comput (ProgramPart s1),s1,1) | (dom p) = (Comput (ProgramPart s2),s2,1) | (dom p) ; :: thesis: contradiction
A14: (Following (ProgramPart s1),s1) | (dom p) = (Following (ProgramPart s1),(Comput (ProgramPart s1),s1,0 )) | (dom p) by AMI_1:13
.= (Comput (ProgramPart s1),s1,(0 + 1)) | (dom p) by AMI_1:14
.= (Following (ProgramPart s2),(Comput (ProgramPart s2),s2,0 )) | (dom p) by A13, AMI_1:14
.= (Following (ProgramPart s2),s2) | (dom p) by AMI_1:13 ;
dom (p +* ((IC p) .--> (goto 0 ))) = (dom p) \/ (dom ((IC p) .--> (goto 0 ))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto 0 ))) by A8, XBOOLE_0:def 3;
then Y: s1 . (IC p) = (p +* ((IC p) .--> (goto 0 ))) . (IC p) by A2, GRFUNC_1:8
.= ((IC p) .--> (goto 0 )) . (IC p) by A8, FUNCT_4:14
.= goto 0 by FUNCOP_1:87 ;
Z: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by AMI_1:150;
y: p c= s1 by A2, A10, XBOOLE_1:1;
then (Following (ProgramPart s1),s1) . (IC SCMPDS ) = (Exec (goto 0 ),s1) . (IC SCMPDS ) by A1, GRFUNC_1:8, Y, Z
.= ICplusConst s1,0 by SCMPDS_2:66 ;
then A15: ICplusConst s1,0 = ((Following (ProgramPart s1),s1) | (dom p)) . (IC SCMPDS ) by A1, FUNCT_1:72
.= ICplusConst s2,1 by A1, A12, A14, FUNCT_1:72 ;
IC s2 = IC p by A1, GRFUNC_1:8, x
.= IC s1 by A1, GRFUNC_1:8, y ;
hence contradiction by A15, Th19; :: thesis: verum

end;

hence contradiction ; :: thesis: verum