let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k)
let s be 0 -started State of SCMPDS; :: thesis: for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k)
let I be parahalting Program of SCMPDS; :: thesis: for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k)
let J be Program of SCMPDS; :: thesis: for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k)
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) )
set spI = stop I;
set P1 = P +* (stop I);
set P2 = P +* (I ';' J);
set n = LifeSpan ((P +* (stop I)),s);
I: Initialize s = s by MEMSTR_0:44;
defpred S₁[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,$1) = Comput ((P +* (I ';' J)),s,$1) );
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: ( m <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,m) = Comput ((P +* (I ';' J)),s,m) ) ; :: thesis: S₁[m + 1]
A4: Comput ((P +* (I ';' J)),s,(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by EXTPRO_1:3;
stop I c= P +* (stop I) by FUNCT_4:25;
then A5: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by SCMPDS_4:def 6;
A6: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3;
assume A7: m + 1 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1))
A9: m < LifeSpan ((P +* (stop I)),s) by A7, NAT_1:13;
then IC (Comput ((P +* (stop I)),s,m)) in dom I by I, Th28;
then A10: IC (Comput ((P +* (stop I)),s,m)) in dom (I ';' J) by FUNCT_4:12;
A11: IC (Comput ((P +* (stop I)),s,m)) in dom I by A9, I, Th28;
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,m))) by PBOOLE:143
.= (stop I) . (IC (Comput ((P +* (stop I)),s,m))) by A5, FUNCT_4:13
.= I . (IC (Comput ((P +* (stop I)),s,m))) by A11, AFINSQ_1:def 3
.= (I ';' J) . (IC (Comput ((P +* (stop I)),s,m))) by A11, AFINSQ_1:def 3
.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),s,m))) by A10, FUNCT_4:13
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by A7, PBOOLE:143, A3, NAT_1:13 ;
hence Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1)) by A3, A7, A6, A4, NAT_1:13; :: thesis: verum

end;

A12: Comput ((P +* (I ';' J)),s,0) = s by EXTPRO_1:2, I;
A15: S₁[ 0 ] by EXTPRO_1:2, A12, I;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A2);
hence ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) ) by I; :: thesis: verum