let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )

let I be really-closed Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA st I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )

let J be Program of SCM+FSA; :: thesis: ( I is_halting_on s,P implies ( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) ) )

A1: dom (P +* ()) = NAT by PARTFUN1:def 2;
A2: dom (P +* (I ";" J)) = NAT by PARTFUN1:def 2;
set s2 = Initialize s;
A3: (Directed I) ";" J = I ";" J ;
set s1 = Initialize s;
assume A4: I is_halting_on s,P ; :: thesis: ( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )

then A5: (LifeSpan ((P +* I),())) + 1 = pseudo-LifeSpan (s,P,()) by Lm2;
A6: Directed I is_pseudo-closed_on s,P by ;
hereby :: thesis: ( DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )
let k be Nat; :: thesis: ( k <= LifeSpan ((P +* I),()) implies ( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) )
assume k <= LifeSpan ((P +* I),()) ; :: thesis: ( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) )
then A7: k < pseudo-LifeSpan (s,P,()) by ;
then A8: IC (Comput ((P +* ()),(),k)) in dom () by ;
Comput ((P +* ()),(),k) = Comput ((P +* (I ";" J)),(),k) by A3, A4, Lm2, A7, Th11;
hence A9: IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) ; :: thesis: CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k)))
A10: Directed I c= I ";" J by SCMFSA6A:16;
then A11: dom () c= dom (I ";" J) by GRFUNC_1:2;
thus CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = (P +* ()) . (IC (Comput ((P +* ()),(),k))) by
.= () . (IC (Comput ((P +* ()),(),k))) by
.= (I ";" J) . (IC (Comput ((P +* ()),(),k))) by
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(),k))) by
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) by ; :: thesis: verum
end;
Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1)) = Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1)) by A4, A3, A5, Lm2, Th11;
hence ( DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) ) ; :: thesis: verum