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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )

A1: dom (P +* (Directed I)) = 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )

then A5: (LifeSpan ((P +* I),(Initialize s))) + 1 = pseudo-LifeSpan (s,P,(Directed I)) by Lm2;

A6: Directed I is_pseudo-closed_on s,P by A4, Lm2;

hence ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) ; :: thesis: verum

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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) )

A1: dom (P +* (Directed I)) = 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),(Initialize s)) holds

( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) ) & DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )

then A5: (LifeSpan ((P +* I),(Initialize s))) + 1 = pseudo-LifeSpan (s,P,(Directed I)) by Lm2;

A6: Directed I is_pseudo-closed_on s,P by A4, Lm2;

hereby :: thesis: ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) )

Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)) = Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))
by A4, A3, A5, Lm2, Th11;let k be Nat; :: thesis: ( k <= LifeSpan ((P +* I),(Initialize s)) implies ( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) ) )

assume k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) )

then A7: k < pseudo-LifeSpan (s,P,(Directed I)) by A5, NAT_1:13;

then A8: IC (Comput ((P +* (Directed I)),(Initialize s),k)) in dom (Directed I) by A6, Def3;

Comput ((P +* (Directed I)),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) by A3, A4, Lm2, A7, Th11;

hence A9: IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) ; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k)))

A10: Directed I c= I ";" J by SCMFSA6A:16;

then A11: dom (Directed I) c= dom (I ";" J) by GRFUNC_1:2;

thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A1, PARTFUN1:def 6

.= (Directed I) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, FUNCT_4:13

.= (I ";" J) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, A10, GRFUNC_1:2

.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k))) by A9, A11, A8, FUNCT_4:13

.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by A2, PARTFUN1:def 6 ; :: thesis: verum

end;assume k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) )

then A7: k < pseudo-LifeSpan (s,P,(Directed I)) by A5, NAT_1:13;

then A8: IC (Comput ((P +* (Directed I)),(Initialize s),k)) in dom (Directed I) by A6, Def3;

Comput ((P +* (Directed I)),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) by A3, A4, Lm2, A7, Th11;

hence A9: IC (Comput ((P +* (Directed I)),(Initialize s),k)) = IC (Comput ((P +* (I ";" J)),(Initialize s),k)) ; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k)))

A10: Directed I c= I ";" J by SCMFSA6A:16;

then A11: dom (Directed I) c= dom (I ";" J) by GRFUNC_1:2;

thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A1, PARTFUN1:def 6

.= (Directed I) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, FUNCT_4:13

.= (I ";" J) . (IC (Comput ((P +* (Directed I)),(Initialize s),k))) by A8, A10, GRFUNC_1:2

.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k))) by A9, A11, A8, FUNCT_4:13

.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by A2, PARTFUN1:def 6 ; :: thesis: verum

hence ( DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) & IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ";" J)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) ; :: thesis: verum