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

proof

take s1 ; :: according to EXTPRO_1:def 9 :: 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,R))) = {(IC p)} by FUNCOP_1:19;
then A6: IC p in dom ((IC p) .--> (goto (1,R))) by TARSKI:def 1;
A7: dom p misses {(IC p)} by A4, ZFMISC_1:56;
then A8: p c= p +* ((IC p) .--> (goto (1,R))) by A5, FUNCT_4:33;
dom (p +* ((IC p) .--> (goto (1,R)))) = (dom p) \/ (dom ((IC p) .--> (goto (1,R)))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto (1,R)))) by A6, XBOOLE_0:def 3;
then X: s2 . (IC p) = (p +* ((IC p) .--> (goto (1,R)))) . (IC p) by A3, GRFUNC_1:8
.= ((IC p) .--> (goto (1,R))) . (IC p) by A6, FUNCT_4:14
.= goto (1,R) by FUNCOP_1:87 ;
Y: (ProgramPart s2) /. (IC p) = s2 . (IC p) by COMPOS_1:38;
p c= s2 by A3, A8, XBOOLE_1:1;
then A9: (Following ((ProgramPart s2),s2)) . (IC (SCM R)) = (Exec ((goto (1,R)),s2)) . (IC (SCM R)) by A1, X, Y, GRFUNC_1:8
.= 1 by SCMRING2:17 ;
A10: dom ((IC p) .--> (goto (0,R))) = {(IC p)} by FUNCOP_1:19;
then A11: IC p in dom ((IC p) .--> (goto (0,R))) by TARSKI:def 1;
A12: p c= p +* ((IC p) .--> (goto (0,R))) by A10, A7, FUNCT_4:33;
hence ( p c= s1 & p c= s2 ) by A2, A3, A8, 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)
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 EXTPRO_1:3
.= (Comput ((ProgramPart s1),s1,(0 + 1))) | (dom p) by EXTPRO_1:4
.= (Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0)))) | (dom p) by A13, EXTPRO_1:4
.= (Following ((ProgramPart s2),s2)) | (dom p) by EXTPRO_1:3 ;
dom (p +* ((IC p) .--> (goto (0,R)))) = (dom p) \/ (dom ((IC p) .--> (goto (0,R)))) by FUNCT_4:def 1;
then IC p in dom (p +* ((IC p) .--> (goto (0,R)))) by A11, XBOOLE_0:def 3;
then X: s1 . (IC p) = (p +* ((IC p) .--> (goto (0,R)))) . (IC p) by A2, GRFUNC_1:8
.= ((IC p) .--> (goto (0,R))) . (IC p) by A11, FUNCT_4:14
.= goto (0,R) by FUNCOP_1:87 ;
Y: (ProgramPart s1) /. (IC p) = s1 . (IC p) by COMPOS_1:38;
p c= s1 by A2, A12, XBOOLE_1:1;
then (Following ((ProgramPart s1),s1)) . (IC (SCM R)) = (Exec ((goto (0,R)),s1)) . (IC (SCM R)) by A1, X, Y, GRFUNC_1:8
.= 0 by SCMRING2:17 ;
then 0 = ((Following ((ProgramPart s1),s1)) | (dom p)) . (IC (SCM R)) by A1, FUNCT_1:72
.= 1 by A1, A9, A14, FUNCT_1:72 ;
hence contradiction ; :: thesis: verum

end;

hence contradiction ; :: thesis: verum