let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; :: according to AMISTD_5:def 4 :: thesis: for p being non empty q -autonomic FinPartState of (STC N)
for s being State of (STC N) st p c= s holds
for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q
let p be non empty q -autonomic FinPartState of (STC N); :: thesis: for s being State of (STC N) st p c= s holds
for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q
let s be State of (STC N); :: thesis: ( p c= s implies for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q )
assume A1: p c= s ; :: thesis: for P being Instruction-Sequence of (STC N) st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q
let P be Instruction-Sequence of (STC N); :: thesis: ( q c= P implies for i being Nat holds IC (Comput (P,s,i)) in dom q )
assume A2: q c= P ; :: thesis: for i being Nat holds IC (Comput (P,s,i)) in dom q
let i be Nat; :: thesis: IC (Comput (P,s,i)) in dom q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume A3: not IC (Comput (P,s,i)) in dom q ; :: thesis: contradiction
the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then reconsider I = [1,0,0] as Instruction of (STC N) by TARSKI:def 2;
set p1 = q +* ((IC (Comput (P,s,i))) .--> I);
set p2 = q +* ((IC (Comput (P,s,i))) .--> (halt (STC N)));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> I) as Instruction-Sequence of (STC N) ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) as Instruction-Sequence of (STC N) ;
A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt (STC N))) by TARSKI:def 1;
A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> I) by TARSKI:def 1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt (STC N))) by A3, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> I) by A3, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> I) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) c= P2 by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
not p is q -autonomic

proof

((IC (Comput (P,s,i))) .--> (halt (STC N))) . (IC (Comput (P,s,i))) = halt (STC N) by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt (STC N) by A5, FUNCT_4:13;
((IC (Comput (P,s,i))) .--> I) . (IC (Comput (P,s,i))) = I by FUNCOP_1:72;
then A13: P1 . (IC (Comput (P,s,i))) = I by A7, FUNCT_4:13;
take P1 ; :: according to EXTPRO_1:def 10 :: thesis: ex b₁ being set st
( q c= P1 & q c= b₁ & ex b₂, b₃ being set st
( p c= b₂ & p c= b₃ & not for b₄ being set holds (Comput (P1,b₂,b₄)) | (proj1 p) = (Comput (b₁,b₃,b₄)) | (proj1 p) ) )
take P2 ; :: thesis: ( q c= P1 & q c= P2 & ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being set holds (Comput (P1,b₁,b₃)) | (proj1 p) = (Comput (P2,b₂,b₃)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> I) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; :: thesis: ( q c= P2 & ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being set holds (Comput (P1,b₁,b₃)) | (proj1 p) = (Comput (P2,b₂,b₃)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> (halt (STC N))) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; :: thesis: ex b₁, b₂ being set st
( p c= b₁ & p c= b₂ & not for b₃ being set holds (Comput (P1,b₁,b₃)) | (proj1 p) = (Comput (P2,b₂,b₃)) | (proj1 p) )
take s ; :: thesis: ex b₁ being set st
( p c= s & p c= b₁ & not for b₂ being set holds (Comput (P1,s,b₂)) | (proj1 p) = (Comput (P2,b₁,b₂)) | (proj1 p) )
take s ; :: thesis: ( p c= s & p c= s & not for b₁ being set holds (Comput (P1,s,b₁)) | (proj1 p) = (Comput (P2,s,b₁)) | (proj1 p) )
thus p c= s by A1; :: thesis: ( p c= s & not for b₁ being set holds (Comput (P1,s,b₁)) | (proj1 p) = (Comput (P2,s,b₁)) | (proj1 p) )
A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def 10;
thus p c= s by A1; :: thesis: not for b₁ being set holds (Comput (P1,s,b₁)) | (proj1 p) = (Comput (P2,s,b₁)) | (proj1 p)
A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def 10;
take k = i + 1; :: thesis: not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p)
set Cs1k = Comput (P1,s,k);
A18: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s,i)))),(Comput (P1,s,i))) ;
InsCode I = 1 ;
then A19: IC (Exec (I,(Comput (P1,s,i)))) = (IC (Comput (P1,s,i))) + 1 by AMISTD_1:9;
A20: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by Th6, FUNCT_1:49;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, Th6, FUNCT_1:49;
then A21: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A19, A18, A13, PBOOLE:143;
set Cs2k = Comput (P2,s,k);
A22: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A23: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;
IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A20, A17, Th6, FUNCT_1:49;
then A24: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A22, A12, A23, EXTPRO_1:def 3;
( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by Th6, FUNCT_1:49;
hence not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p) by A21, A24; :: thesis: verum

end;

hence contradiction ; :: thesis: verum