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 ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) & Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT )
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 implies ( LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) & Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) 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 ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) & Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT ) )
set ss2 = s2 +* (I +* (Start-At (0,SCM+FSA)));
set ss1 = s1 +* (I +* (Start-At (0,SCM+FSA)));
assume A2: I is_halting_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or ( LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) & Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT ) )
then A3: ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s1 +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
then A4: Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))))) by EXTPRO_1:23;
assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) & Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT )
then I is_halting_on s2 by A1, A2, SCMFSA8B:8;
then A6: ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) halts_on s2 +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;

A7: now

let l be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),l))) = halt SCM+FSA implies LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) <= l )
TX2: ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),l)) by AMI_1:123;
TX1: ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),l)) by AMI_1:123;
assume A8: CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),l))) = halt SCM+FSA ; :: thesis: LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) <= l
CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),l))) = CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),l))) by A1, A2, A5, Th100, TX1, TX2;
hence LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) <= l by A3, A8, EXTPRO_1:def 14; :: thesis: verum

end;

TX2: ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
TX1: ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
CurInstr ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))))))) = CurInstr ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))))))) by A1, A2, A5, Th100, TX1, TX2
.= halt SCM+FSA by A3, EXTPRO_1:def 14 ;
hence LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))) = LifeSpan ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) by A7, A6, EXTPRO_1:def 14; :: thesis: Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT
then Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) = Comput ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))))) by A6, EXTPRO_1:23;
hence Result ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA))))), Result ((ProgramPart (s2 +* (I +* (Start-At (0,SCM+FSA))))),(s2 +* (I +* (Start-At (0,SCM+FSA))))) equal_outside NAT by A1, A2, A5, A4, Th100; :: thesis: verum