let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of SCMPDS
for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let I, J be Program of SCMPDS; :: thesis: for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
let k be Element of NAT ; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) )
set spI = stop I;
set s1 = Initialize s;
set P1 = P +* (stop I);
set s2 = Initialize s;
set P2 = P +* (I ';' J);
set n = LifeSpan ((P +* (stop I)),(Initialize s));
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: ( not k <= LifeSpan ((P +* (stop I)),(Initialize s)) or Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) )
assume A3: k <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k)
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* (stop I)),(Initialize s),$1) = Comput ((P +* (I ';' J)),(Initialize s),$1) );
A4: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: ( m <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* (stop I)),(Initialize s),m) = Comput ((P +* (I ';' J)),(Initialize s),m) ) ; :: thesis: S₁[m + 1]
A7: Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m)))),(Comput ((P +* (stop I)),(Initialize s),m))) ;
A8: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A1, SCMPDS_6:def 2;
A10: Comput ((P +* (I ';' J)),(Initialize s),(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m)))),(Comput ((P +* (I ';' J)),(Initialize s),m))) ;
assume A11: m + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(m + 1))
then m < LifeSpan ((P +* (stop I)),(Initialize s)) by NAT_1:13;
then A12: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by A1, A2, SCMPDS_6:26;
then A13: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (I ';' J) by FUNCT_4:12;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A8, FUNCT_4:13
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A12, AFINSQ_1:def 3
.= (I ';' J) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A12, AFINSQ_1:def 3
.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A13, FUNCT_4:13
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by A5, A11, PBOOLE:143, NAT_1:13 ;
hence Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(m + 1)) by A5, A11, A10, A7, NAT_1:13; :: thesis: verum

end;

A16: Comput ((P +* (I ';' J)),(Initialize s),0) = Initialize s by EXTPRO_1:2;
A19: S₁[ 0 ] by EXTPRO_1:2, A16;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A19, A4);
hence Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) by A3; :: thesis: verum