let s1, s2 be State of SCM+FSA; :: thesis: for p1, p2 being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

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

assume that

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

A2: Initialize ((intloc 0) .--> 1) c= s2 and

A3: I c= p1 and

A4: I c= p2 and

A5: s1 = s2 ; :: thesis: ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

A6: p2 halts_on s2 by A2, Def1, A4;

A7: p1 halts_on s1 by A1, Def1, A3;

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

hence A10: LifeSpan (p1,s1) = LifeSpan (p2,s2) by A8, A6, EXTPRO_1:def 15; :: thesis: Result (p1,s1) = Result (p2,s2)

p2 halts_on s2 by A2, Def1, A4;

then A11: Result (p2,s2) = Comput (p2,s2,(LifeSpan (p1,s1))) by A10, EXTPRO_1:23;

p1 halts_on s1 by A1, Def1, A3;

then Result (p1,s1) = Comput (p1,s1,(LifeSpan (p1,s1))) by EXTPRO_1:23;

hence Result (p1,s1) = Result (p2,s2) by A1, A5, A11, Th5, A3, A4; :: thesis: verum

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

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

assume that

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

A2: Initialize ((intloc 0) .--> 1) c= s2 and

A3: I c= p1 and

A4: I c= p2 and

A5: s1 = s2 ; :: thesis: ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

A6: p2 halts_on s2 by A2, Def1, A4;

A7: p1 halts_on s1 by A1, Def1, A3;

A8: now :: thesis: for l being Nat st CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA holds

LifeSpan (p1,s1) <= l

CurInstr (p2,(Comput (p2,s2,(LifeSpan (p1,s1))))) =
CurInstr (p1,(Comput (p1,s1,(LifeSpan (p1,s1)))))
by A1, A5, Th5, A3, A4
LifeSpan (p1,s1) <= l

let l be Nat; :: thesis: ( CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA implies LifeSpan (p1,s1) <= l )

assume A9: CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA ; :: thesis: LifeSpan (p1,s1) <= l

CurInstr (p1,(Comput (p1,s1,l))) = CurInstr (p2,(Comput (p2,s2,l))) by A1, A5, Th5, A3, A4;

hence LifeSpan (p1,s1) <= l by A7, A9, EXTPRO_1:def 15; :: thesis: verum

end;assume A9: CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA ; :: thesis: LifeSpan (p1,s1) <= l

CurInstr (p1,(Comput (p1,s1,l))) = CurInstr (p2,(Comput (p2,s2,l))) by A1, A5, Th5, A3, A4;

hence LifeSpan (p1,s1) <= l by A7, A9, EXTPRO_1:def 15; :: thesis: verum

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

hence A10: LifeSpan (p1,s1) = LifeSpan (p2,s2) by A8, A6, EXTPRO_1:def 15; :: thesis: Result (p1,s1) = Result (p2,s2)

p2 halts_on s2 by A2, Def1, A4;

then A11: Result (p2,s2) = Comput (p2,s2,(LifeSpan (p1,s1))) by A10, EXTPRO_1:23;

p1 halts_on s1 by A1, Def1, A3;

then Result (p1,s1) = Comput (p1,s1,(LifeSpan (p1,s1))) by EXTPRO_1:23;

hence Result (p1,s1) = Result (p2,s2) by A1, A5, A11, Th5, A3, A4; :: thesis: verum