set D = Int-Locations \/ FinSeq-Locations ;
let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 holds
( LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) & Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 implies ( LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) & Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT ) )
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not DataPart s1 = DataPart s2 or ( LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) & Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT ) )
assume A2: I is_halting_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) & Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT ) )
assume A3: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) & Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT )
set ss1 = s1 +* (I +* (Start-At (insloc 0 )));
set ss2 = s2 +* (I +* (Start-At (insloc 0 )));
A4: s1 +* (I +* (Start-At (insloc 0 ))) is halting by A2, SCMFSA7B:def 8;

A5: now

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

end;

A7: CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))))) = CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))))) by A1, A2, A3, Th100
.= halt SCM+FSA by A4, AMI_1:def 46 ;
I is_halting_on s2 by A1, A2, A3, SCMFSA8B:8;
then A8: s2 +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
hence LifeSpan (s1 +* (I +* (Start-At (insloc 0 )))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0 )))) by A5, A7, AMI_1:def 46; :: thesis: Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT
then A9: Result (s2 +* (I +* (Start-At (insloc 0 )))) = Computation (s2 +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s1 +* (I +* (Start-At (insloc 0 ))))) by A8, AMI_1:122;
Result (s1 +* (I +* (Start-At (insloc 0 )))) = Computation (s1 +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s1 +* (I +* (Start-At (insloc 0 ))))) by A4, AMI_1:122;
hence Result (s1 +* (I +* (Start-At (insloc 0 )))), Result (s2 +* (I +* (Start-At (insloc 0 )))) equal_outside NAT by A1, A2, A3, A9, Th100; :: thesis: verum