let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),()) holds
Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k)

let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of
for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),()) holds
Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k)

let I, J be Program of ; :: thesis: for k being Nat st I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),()) holds
Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k)

let k be Nat; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),()) implies Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),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)),());
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P ; :: thesis: ( not k <= LifeSpan ((P +* (stop I)),()) or Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k) )
assume A3: k <= LifeSpan ((P +* (stop I)),()) ; :: thesis: Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k)
defpred S1[ Nat] means ( \$1 <= LifeSpan ((P +* (stop I)),()) implies Comput ((P +* (stop I)),(),\$1) = Comput ((P +* (I ';' J)),(),\$1) );
A4: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A5: ( m <= LifeSpan ((P +* (stop I)),()) implies Comput ((P +* (stop I)),(),m) = Comput ((P +* (I ';' J)),(),m) ) ; :: thesis: S1[m + 1]
A6: Comput ((P +* (stop I)),(),(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),(),m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),m)))),(Comput ((P +* (stop I)),(),m))) ;
A7: IC (Comput ((P +* (stop I)),(),m)) in dom (stop I) by ;
A8: Comput ((P +* (I ';' J)),(),(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(),m))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(),m)))),(Comput ((P +* (I ';' J)),(),m))) ;
assume A9: m + 1 <= LifeSpan ((P +* (stop I)),()) ; :: thesis: Comput ((P +* (stop I)),(),(m + 1)) = Comput ((P +* (I ';' J)),(),(m + 1))
then m < LifeSpan ((P +* (stop I)),()) by NAT_1:13;
then A10: IC (Comput ((P +* (stop I)),(),m)) in dom I by ;
then A11: IC (Comput ((P +* (stop I)),(),m)) in dom (I ';' J) by FUNCT_4:12;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(),m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(),m))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),(),m))) by
.= I . (IC (Comput ((P +* (stop I)),(),m))) by
.= (I ';' J) . (IC (Comput ((P +* (stop I)),(),m))) by
.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(),m))) by
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(),m))) by ;
hence Comput ((P +* (stop I)),(),(m + 1)) = Comput ((P +* (I ';' J)),(),(m + 1)) by A5, A9, A8, A6, NAT_1:13; :: thesis: verum
end;
A12: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A12, A4);
hence Comput ((P +* (stop I)),(),k) = Comput ((P +* (I ';' J)),(),k) by A3; :: thesis: verum