let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of st 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 parahalting Program of st stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

let I be parahalting Program of ; :: thesis: ( stop I c= P1 & stop I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )
set SI = stop I;
assume that
A1: stop I c= P1 and
A2: stop I c= P2 ; :: thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
A3: P2 halts_on s by ;
A4: P1 halts_on s by ;
A5: now :: thesis: for l being Nat st CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS holds
LifeSpan (P1,s) <= l
let l be Nat; :: thesis: ( CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS implies LifeSpan (P1,s) <= l )
assume A6: 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, A2, Th5;
hence LifeSpan (P1,s) <= l by ; :: thesis: verum
end;
CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) = CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s))))) by A1, A2, Th5
.= halt SCMPDS by ;
hence A7: LifeSpan (P1,s) = LifeSpan (P2,s) by ; :: thesis: Result (P1,s) = Result (P2,s)
P2 halts_on s by ;
then A8: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by ;
P1 halts_on s by ;
then Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23;
hence Result (P1,s) = Result (P2,s) by A1, A2, A8, Th5; :: thesis: verum