let s1, s2 be State of SCM+FSA ; :: thesis: for I being parahalting Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 & Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT )
let I be parahalting Program of SCM+FSA ; :: thesis: ( I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT implies ( LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 & Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT ) )
assume that
A1: I +* (Start-At 0 ,SCM+FSA ) c= s1 and
A2: I +* (Start-At 0 ,SCM+FSA ) c= s2 and
A3: s1,s2 equal_outside NAT ; :: thesis: ( LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 & Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT )
A4: ProgramPart s2 halts_on s2 by A2, Th18;
A5: ProgramPart s1 halts_on s1 by A1, Th18;

A6: now

let l be Element of NAT ; :: thesis: ( CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,l) = halt SCM+FSA implies LifeSpan (ProgramPart s1),s1 <= l )
TX: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,l) by AMI_1:123;
TY: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,l) by AMI_1:123;
assume A7: CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,l) = halt SCM+FSA ; :: thesis: LifeSpan (ProgramPart s1),s1 <= l
CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,l) = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,l) by A1, A2, A3, Th28, TX, TY;
hence LifeSpan (ProgramPart s1),s1 <= l by A5, A7, AMI_1:def 46; :: thesis: verum

end;

TL: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
TL1: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) by AMI_1:123;
CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1)) = CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1)) by A1, A2, A3, Th28, TL, TL1
.= halt SCM+FSA by A5, AMI_1:def 46 ;
hence K: LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 by A6, A4, AMI_1:def 46; :: thesis: Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT
ProgramPart s2 halts_on s2 by A2, Th18;
then A8: Result (ProgramPart s2),s2 = Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart s1),s1) by K, AMI_1:122;
ProgramPart s1 halts_on s1 by A1, Th18;
then Result (ProgramPart s1),s1 = Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1) by AMI_1:122;
hence Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT by A1, A2, A3, A8, Th28; :: thesis: verum