let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

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

let s be State of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

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

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )

assume that

A1: Initialize ((intloc 0) .--> 1) c= s and

A2: I c= P1 and

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

A4: P2 halts_on s by A1, A3, Def1;

A5: P1 halts_on s by A1, A2, Def1;

.= halt SCM+FSA by A5, EXTPRO_1:def 15 ;

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

thus Result (P1,s) = Result (P2,s) by A1, Th6, A2, A3; :: thesis: verum

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

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

let s be State of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

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

let I be really-closed InitHalting Program of SCM+FSA; :: thesis: ( Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )

assume that

A1: Initialize ((intloc 0) .--> 1) c= s and

A2: I c= P1 and

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

A4: P2 halts_on s by A1, A3, Def1;

A5: P1 halts_on s by A1, A2, Def1;

A6: now :: thesis: for l being Nat st CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA holds

LifeSpan (P1,s) <= l

CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) =
CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s)))))
by A1, Lm4, A2, A3
LifeSpan (P1,s) <= l

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

assume A7: 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 A1, Lm4, A2, A3;

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

end;assume A7: 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 A1, Lm4, A2, A3;

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

.= halt SCM+FSA by A5, EXTPRO_1:def 15 ;

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

thus Result (P1,s) = Result (P2,s) by A1, Th6, A2, A3; :: thesis: verum