let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)
let I, J be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k) )
set s1 = Initialize s;
set s2 = Initialize s;
defpred S₁[ Nat] means ( $1 <= pseudo-LifeSpan (s,P,I) implies Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (I ";" J)),(Initialize s),$1) );
A1: dom (P +* I) = NAT by PARTFUN1:def 2;
A2: dom (P +* (I ";" J)) = NAT by PARTFUN1:def 2;
assume A3: I is_pseudo-closed_on s,P ; :: thesis: for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ";" J)),(Initialize s),k)

A4: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

A6: Comput ((P +* (I ";" J)),(Initialize s),(k + 1)) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k)))),(Comput ((P +* (I ";" J)),(Initialize s),k))) ;
A7: Comput ((P +* I),(Initialize s),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k))) ;
A8: dom I c= dom (I ";" J) by SCMFSA6A:17;
A9: k + 0 < k + 1 by XREAL_1:6;
assume A10: k + 1 <= pseudo-LifeSpan (s,P,I) ; :: thesis: Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (I ";" J)),(Initialize s),(k + 1))
then A11: k < pseudo-LifeSpan (s,P,I) by A9, XXREAL_0:2;
then A12: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A3, Th10;
A13: I c= P +* I by FUNCT_4:25;
A14: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
A15: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A1, PARTFUN1:def 6
.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A12, A13, GRFUNC_1:2 ;
then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A3, A11, Th10;
then CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (I ";" J) . (IC (Comput ((P +* I),(Initialize s),k))) by A12, A15, SCMFSA6A:15
.= (P +* (I ";" J)) . (IC (Comput ((P +* I),(Initialize s),k))) by A12, A8, A14, GRFUNC_1:2
.= (P +* (I ";" J)) . (IC (Comput ((P +* (I ";" J)),(Initialize s),k))) by A5, A10, A9, XXREAL_0:2
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(Initialize s),k))) by A2, PARTFUN1:def 6 ;
hence Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (I ";" J)),(Initialize s),(k + 1)) by A5, A10, A9, A7, A6, XXREAL_0:2; :: thesis: verum

end;

end;

A16: S₁[ 0 ] ;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A16, A4); :: thesis: verum