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

for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

let s be 0 -started State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

let I be Program of ; :: thesis: ( I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )

assume that

A1: I is_closed_on s,P1 and

A2: I is_halting_on s,P1 and

A3: stop I c= P1 and

A4: stop I c= P2 ; :: thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

A5: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;

A6: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;

DataPart s = DataPart s ;

then A7: I is_halting_on s,P2 by A1, A2, SCMPDS_6:23;

A8: Initialize s = s by A5, FUNCT_4:98;

A9: Initialize s = s by A6, FUNCT_4:98;

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

then A10: P2 halts_on s by A7, A9, SCMPDS_6:def 3;

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

then A11: P1 halts_on s by A2, A8, SCMPDS_6:def 3;

.= halt SCMPDS by A11, EXTPRO_1:def 15 ;

hence LifeSpan (P1,s) = LifeSpan (P2,s) by A12, A10, EXTPRO_1:def 15; :: thesis: Result (P1,s) = Result (P2,s)

then A14: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by A10, EXTPRO_1:23;

Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by A11, EXTPRO_1:23;

hence Result (P1,s) = Result (P2,s) by A1, A3, A4, A14, Th7; :: thesis: verum

for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

let s be 0 -started State of SCMPDS; :: thesis: for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

let I be Program of ; :: thesis: ( I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )

assume that

A1: I is_closed_on s,P1 and

A2: I is_halting_on s,P1 and

A3: stop I c= P1 and

A4: stop I c= P2 ; :: thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

A5: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;

A6: Start-At (0,SCMPDS) c= s by MEMSTR_0:29;

DataPart s = DataPart s ;

then A7: I is_halting_on s,P2 by A1, A2, SCMPDS_6:23;

A8: Initialize s = s by A5, FUNCT_4:98;

A9: Initialize s = s by A6, FUNCT_4:98;

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

then A10: P2 halts_on s by A7, A9, SCMPDS_6:def 3;

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

then A11: P1 halts_on s by A2, A8, SCMPDS_6:def 3;

A12: now :: thesis: for l being Nat st CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS holds

LifeSpan (P1,s) <= l

CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) =
CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s)))))
by A1, A3, A4, Th7
LifeSpan (P1,s) <= l

let l be Nat; :: thesis: ( CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS implies LifeSpan (P1,s) <= l )

assume A13: CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS ; :: thesis: LifeSpan (P1,s) <= l

CurInstr (P1,(Comput (P1,s,l))) = CurInstr (P2,(Comput (P2,s,l))) by A1, A3, A4, Th7;

hence LifeSpan (P1,s) <= l by A11, A13, EXTPRO_1:def 15; :: thesis: verum

end;assume A13: CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS ; :: thesis: LifeSpan (P1,s) <= l

CurInstr (P1,(Comput (P1,s,l))) = CurInstr (P2,(Comput (P2,s,l))) by A1, A3, A4, Th7;

hence LifeSpan (P1,s) <= l by A11, A13, EXTPRO_1:def 15; :: thesis: verum

.= halt SCMPDS by A11, EXTPRO_1:def 15 ;

hence LifeSpan (P1,s) = LifeSpan (P2,s) by A12, A10, EXTPRO_1:def 15; :: thesis: Result (P1,s) = Result (P2,s)

then A14: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by A10, EXTPRO_1:23;

Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by A11, EXTPRO_1:23;

hence Result (P1,s) = Result (P2,s) by A1, A3, A4, A14, Th7; :: thesis: verum