let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being 0 -started State of SCMPDS

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

let s1, s2 be 0 -started State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

let I be Program of ; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 implies Result (P1,s1) = Result (P2,s2) )

set pI = stop I;

assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not stop I c= P1 or not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

assume A2: I is_halting_on s1,P1 ; :: thesis: ( not stop I c= P1 or not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

assume stop I c= P1 ; :: thesis: ( not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

then A3: P1 = P1 +* (stop I) by FUNCT_4:98;

assume stop I c= P2 ; :: thesis: ( for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

then A4: P2 = P2 +* (stop I) by FUNCT_4:98;

A5: s1 = Initialize s1 by MEMSTR_0:44;

then A6: P1 halts_on s1 by A2, A3, SCMPDS_6:def 3;

then consider n being Nat such that

A7: CurInstr (P1,(Comput (P1,s1,n))) = halt SCMPDS ;

A8: s2 = Initialize s2 by MEMSTR_0:44;

given k being Nat such that A9: Comput (P1,s1,k) = s2 ; :: thesis: Result (P1,s1) = Result (P2,s2)

set s3 = Comput (P1,s1,k);

set P3 = P1;

A10: IC in dom (Comput (P1,s1,k)) by MEMSTR_0:2;

IC (Comput (P1,s1,k)) = 0 by A9, MEMSTR_0:def 11;

then Start-At (0,SCMPDS) c= Comput (P1,s1,k) by A10, FUNCOP_1:73;

then A11: Comput (P1,s1,k) = Initialize (Comput (P1,s1,k)) by FUNCT_4:98;

.= CurInstr (P1,(Comput (P1,s1,n))) by A7, EXTPRO_1:5, NAT_1:11 ;

then P1 halts_on Comput (P1,s1,k) by A7, EXTPRO_1:29;

then A13: I is_halting_on Comput (P1,s1,k),P1 by A11, A3, SCMPDS_6:def 3;

A14: DataPart (Comput (P1,s1,k)) = DataPart s2 by A9;

consider k being Nat such that

A15: CurInstr (P1,(Comput (P1,s1,k))) = halt SCMPDS by A6;

A16: P1 . (IC (Comput (P1,s1,k))) = halt SCMPDS by A15, PBOOLE:143;

I is_closed_on Comput (P1,s1,k),P1 by A11, A12, A3, SCMPDS_6:def 2;

then Result (P1,(Comput (P1,s1,k))) = Result (P2,s2) by A8, A14, A11, A13, Th9, A4, A3;

hence Result (P1,s1) = Result (P2,s2) by A16, EXTPRO_1:8; :: thesis: verum

for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

let s1, s2 be 0 -started State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

let I be Program of ; :: thesis: ( I is_closed_on s1,P1 & I is_halting_on s1,P1 & stop I c= P1 & stop I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 implies Result (P1,s1) = Result (P2,s2) )

set pI = stop I;

assume A1: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or not stop I c= P1 or not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

assume A2: I is_halting_on s1,P1 ; :: thesis: ( not stop I c= P1 or not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

assume stop I c= P1 ; :: thesis: ( not stop I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

then A3: P1 = P1 +* (stop I) by FUNCT_4:98;

assume stop I c= P2 ; :: thesis: ( for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )

then A4: P2 = P2 +* (stop I) by FUNCT_4:98;

A5: s1 = Initialize s1 by MEMSTR_0:44;

then A6: P1 halts_on s1 by A2, A3, SCMPDS_6:def 3;

then consider n being Nat such that

A7: CurInstr (P1,(Comput (P1,s1,n))) = halt SCMPDS ;

A8: s2 = Initialize s2 by MEMSTR_0:44;

given k being Nat such that A9: Comput (P1,s1,k) = s2 ; :: thesis: Result (P1,s1) = Result (P2,s2)

set s3 = Comput (P1,s1,k);

set P3 = P1;

A10: IC in dom (Comput (P1,s1,k)) by MEMSTR_0:2;

IC (Comput (P1,s1,k)) = 0 by A9, MEMSTR_0:def 11;

then Start-At (0,SCMPDS) c= Comput (P1,s1,k) by A10, FUNCOP_1:73;

then A11: Comput (P1,s1,k) = Initialize (Comput (P1,s1,k)) by FUNCT_4:98;

A12: now :: thesis: for n being Nat holds IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I)

CurInstr (P1,(Comput (P1,(Comput (P1,s1,k)),n))) =
CurInstr (P1,(Comput (P1,s1,(k + n))))
by EXTPRO_1:4
let n be Nat; :: thesis: IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I)

IC (Comput (P1,(Comput (P1,s1,k)),n)) = IC (Comput (P1,s1,(k + n))) by EXTPRO_1:4;

hence IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I) by A1, A3, A5, SCMPDS_6:def 2; :: thesis: verum

end;IC (Comput (P1,(Comput (P1,s1,k)),n)) = IC (Comput (P1,s1,(k + n))) by EXTPRO_1:4;

hence IC (Comput (P1,(Comput (P1,s1,k)),n)) in dom (stop I) by A1, A3, A5, SCMPDS_6:def 2; :: thesis: verum

.= CurInstr (P1,(Comput (P1,s1,n))) by A7, EXTPRO_1:5, NAT_1:11 ;

then P1 halts_on Comput (P1,s1,k) by A7, EXTPRO_1:29;

then A13: I is_halting_on Comput (P1,s1,k),P1 by A11, A3, SCMPDS_6:def 3;

A14: DataPart (Comput (P1,s1,k)) = DataPart s2 by A9;

consider k being Nat such that

A15: CurInstr (P1,(Comput (P1,s1,k))) = halt SCMPDS by A6;

A16: P1 . (IC (Comput (P1,s1,k))) = halt SCMPDS by A15, PBOOLE:143;

I is_closed_on Comput (P1,s1,k),P1 by A11, A12, A3, SCMPDS_6:def 2;

then Result (P1,(Comput (P1,s1,k))) = Result (P2,s2) by A8, A14, A11, A13, Th9, A4, A3;

hence Result (P1,s1) = Result (P2,s2) by A16, EXTPRO_1:8; :: thesis: verum