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 AMI_1:122;
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, AMI_1:def 46; :: 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, AMI_1:def 46 ;
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, AMI_1:def 46; :: 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, AMI_1:122;
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