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 Element of 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 Element of 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 Element of 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) );
A2: dom (P +* I) = NAT by PARTFUN1:def 2;
A3: dom (P +* (I ';' J)) = NAT by PARTFUN1:def 2;
assume A4: I is_pseudo-closed_on s,P ; :: thesis: for k being Element of NAT st k <= pseudo-LifeSpan (s,P,I) holds
Comput ((P +* I),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)

A5: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

A7: 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))) ;
A8: 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))) ;
A9: dom I c= dom (I ';' J) by SCMFSA6A:17;
A10: k + 0 < k + 1 by XREAL_1:6;
assume A11: k + 1 <= pseudo-LifeSpan (s,P,I) ; :: thesis: Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(k + 1))
then A12: k < pseudo-LifeSpan (s,P,I) by A10, XXREAL_0:2;
then A13: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A4, Th31;
A14: I c= P +* I by FUNCT_4:25;
A15: I ';' J c= P +* (I ';' J) by FUNCT_4:25;
A16: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) by A2, PARTFUN1:def 6
.= I . (IC (Comput ((P +* I),(Initialize s),k))) by A13, A14, GRFUNC_1:2 ;
then I . (IC (Comput ((P +* I),(Initialize s),k))) <> halt SCM+FSA by A4, A12, Th31;
then CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),k))) = (I ';' J) . (IC (Comput ((P +* I),(Initialize s),k))) by A13, A16, SCMFSA6A:15
.= (P +* (I ';' J)) . (IC (Comput ((P +* I),(Initialize s),k))) by A13, A9, A15, GRFUNC_1:2
.= (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(Initialize s),k))) by A6, A11, A10, XXREAL_0:2
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),k))) by A3, PARTFUN1:def 6 ;
hence Comput ((P +* I),(Initialize s),(k + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(k + 1)) by A6, A11, A10, A8, A7, XXREAL_0:2; :: thesis: verum

end;

end;

A17: S₁[ 0 ]

proof

assume 0 <= pseudo-LifeSpan (s,P,I) ; :: thesis: Comput ((P +* I),(Initialize s),0) = Comput ((P +* (I ';' J)),(Initialize s),0)
Comput ((P +* I),(Initialize s),0) = Initialize s by EXTPRO_1:2;
hence Comput ((P +* I),(Initialize s),0) = Comput ((P +* (I ';' J)),(Initialize s),0) by EXTPRO_1:2; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A17, A5); :: thesis: verum