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

A5: now

let l be Element of NAT ; :: thesis: ( CurInstr (Computation s2,l) = halt SCM+FSA implies LifeSpan s1 <= l )
assume A6: CurInstr (Computation s2,l) = halt SCM+FSA ; :: thesis: LifeSpan s1 <= l
CurInstr (Computation s1,l) = CurInstr (Computation s2,l) by A1, A2, A3, Th28;
hence LifeSpan s1 <= l by A4, A6, AMI_1:def 46; :: thesis: verum

end;

A7: CurInstr (Computation s2,(LifeSpan s1)) = CurInstr (Computation s1,(LifeSpan s1)) by A1, A2, A3, Th28
.= halt SCM+FSA by A4, AMI_1:def 46 ;
s2 is halting by A2, Th18;
hence LifeSpan s1 = LifeSpan s2 by A5, A7, AMI_1:def 46; :: thesis: Result s1, Result s2 equal_outside NAT
then A8: Result s2 = Computation s2,(LifeSpan s1) by A2, Th18, AMI_1:122;
Result s1 = Computation s1,(LifeSpan s1) by A1, Th18, AMI_1:122;
hence Result s1, Result s2 equal_outside NAT by A1, A2, A3, A8, Th28; :: thesis: verum