let q be NAT -defined the InstructionsF of SCMPDS -valued finite non halt-free Function; :: according to AMISTD_5:def 4 :: thesis: for b1 being set
for b2 being set holds
( not b1 c= b2 or for b3 being set holds
( not q c= b3 or for b4 being set holds IC (Comput (b3,b2,b4)) in dom q ) )
let p be non empty q -autonomic FinPartState of SCMPDS; :: thesis: for b1 being set holds
( not p c= b1 or for b2 being set holds
( not q c= b2 or for b3 being set holds IC (Comput (b2,b1,b3)) in dom q ) )
let s be State of SCMPDS; :: thesis: ( not p c= s or for b1 being set holds
( not q c= b1 or for b2 being set holds IC (Comput (b1,s,b2)) in dom q ) )
assume A1: p c= s ; :: thesis: for b1 being set holds
( not q c= b1 or for b2 being set holds IC (Comput (b1,s,b2)) in dom q )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not q c= P or for b1 being set holds IC (Comput (P,s,b1)) in dom q )
assume A2: q c= P ; :: thesis: for b1 being set holds IC (Comput (P,s,b1)) 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 not IC (Comput (P,s,i)) in dom q ; :: thesis: contradiction
then A3: not IC (Comput (P,s,i)) in dom q ;
set I = the Int_position := 0;
set q1 = q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0));
set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) as Instruction-Sequence of SCMPDS ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) as Instruction-Sequence of SCMPDS ;
A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by TARSKI:def 1;
A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by TARSKI:def 1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by A3, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by A3, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) 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 SCMPDS)) . (IC (Comput (P,s,i))) = halt SCMPDS by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt SCMPDS by A5, FUNCT_4:13;
((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) . (IC (Comput (P,s,i))) = the Int_position := 0 by FUNCOP_1:72;
then A13: P1 . (IC (Comput (P,s,i))) = the Int_position := 0 by A7, FUNCT_4:13;
take P1 ; :: according to EXTPRO_1:def 10 :: thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being set holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) )
take P2 ; :: thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> ( the Int_position := 0)) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; :: thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> (halt SCMPDS)) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; :: thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being set holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) )
take s ; :: thesis: ex b1 being set st
( p c= s & p c= b1 & not for b2 being set holds (Comput (P1,s,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) )
take s ; :: thesis: ( p c= s & p c= s & not for b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) )
thus p c= s by A1; :: thesis: ( p c= s & not for b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom 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 b1 being set holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom 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)) | (dom p) = (Comput (P2,s,k)) | (dom p)
set Cs1k = Comput (P1,s,k);
A18: IC in dom p by AMISTD_5:6;
IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;
then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143
.= the Int_position := 0 by A13 ;
A20: 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)))
.= Exec (( the Int_position := 0),(Comput (P1,s,i))) by A19 ;
A21: IC (Exec (( the Int_position := 0),(Comput (P1,s,i)))) = (IC (Comput (P1,s,i))) + 1 by SCMPDS_2:45;
A22: IC in dom p by AMISTD_5:6;
A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A22, FUNCT_1:49;
then A24: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A20, A21
.= (IC (Comput (P,s,i))) + 1 ;
set Cs2k = Comput (P2,s,k);
A25: 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))) ;
A26: 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, A23, A17, A22, FUNCT_1:49;
then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, 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 A22, FUNCT_1:49;
hence not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; :: thesis: verum
end;
hence contradiction ; :: thesis: verum