let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being 0 -started State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)
let s1, s2 be 0 -started State of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)
let J be really-closed Program of SCM+FSA; :: thesis: ( J is_halting_on s1,P1 & J c= P1 & J c= P2 & DataPart s1 = DataPart s2 implies LifeSpan (P1,s1) = LifeSpan (P2,s2) )
assume that
A1: J is_halting_on s1,P1 and
A2: J c= P1 and
A3: J c= P2 and
A4: DataPart s1 = DataPart s2 ; :: thesis: LifeSpan (P1,s1) = LifeSpan (P2,s2)
A5: P1 = P1 +* J by A2, FUNCT_4:98;
s1 = Initialize s1 by MEMSTR_0:44;
then A6: P1 halts_on s1 by A1, A5;
A7: now :: thesis: for k being Nat st CurInstr (P2,(Comput (P2,s2,k))) = halt SCM+FSA holds
LifeSpan (P1,s1) <= k
let k be Nat; :: thesis: ( CurInstr (P2,(Comput (P2,s2,k))) = halt SCM+FSA implies LifeSpan (P1,s1) <= k )
assume CurInstr (P2,(Comput (P2,s2,k))) = halt SCM+FSA ; :: thesis: LifeSpan (P1,s1) <= k
then CurInstr (P1,(Comput (P1,s1,k))) = halt SCM+FSA by A4, Th9, A2, A3;
hence LifeSpan (P1,s1) <= k by A6, EXTPRO_1:def 15; :: thesis: verum
end;
CurInstr (P1,(Comput (P1,s1,(LifeSpan (P1,s1))))) = halt SCM+FSA by A6, EXTPRO_1:def 15;
then A8: CurInstr (P2,(Comput (P2,s2,(LifeSpan (P1,s1))))) = halt SCM+FSA by A4, Th9, A2, A3;
then P2 halts_on s2 by EXTPRO_1:29;
hence LifeSpan (P1,s1) = LifeSpan (P2,s2) by A8, A7, EXTPRO_1:def 15; :: thesis: verum