let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let s be 0 -started State of SCM+FSA; :: thesis: for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let I be parahalting Program of ; :: thesis: ( I c= P1 & I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )
assume that
A1: I c= P1 and
A2: I c= P2 ; :: thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
A6: P2 halts_on s by A2, AMISTD_1:def 11;
A7: P1 halts_on s by A1, AMISTD_1:def 11;

A8: now

let l be Element of NAT ; :: thesis: ( CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA implies LifeSpan (P1,s) <= l )
assume A9: CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA ; :: thesis: LifeSpan (P1,s) <= l
CurInstr (P1,(Comput (P1,s,l))) = CurInstr (P2,(Comput (P2,s,l))) by Th28, A1, A2;
hence LifeSpan (P1,s) <= l by A7, A9, EXTPRO_1:def 15; :: thesis: verum

end;

CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) = CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s))))) by Th28, A1, A2
.= halt SCM+FSA by A7, EXTPRO_1:def 15 ;
hence A10: LifeSpan (P1,s) = LifeSpan (P2,s) by A8, A6, EXTPRO_1:def 15; :: thesis: Result (P1,s) = Result (P2,s)
A11: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by A10, Th18, A2, EXTPRO_1:23;
Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by Th18, A1, EXTPRO_1:23;
hence Result (P1,s) = Result (P2,s) by A11, Th28, A1, A2; :: thesis: verum