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)),(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

for k being 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 ; :: thesis: for k being 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 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_{1}[ 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 Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A12, A4);

hence Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) by A3; :: thesis: verum

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)),(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

for k being 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 ; :: thesis: for k being 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 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

A4: for m being Nat st S

S

proof

A12:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[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_{1}[m + 1]

A6: 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))) ;

A7: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A1, SCMPDS_6:def 2;

A8: 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 A9: 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 A10: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by A1, A2, SCMPDS_6:26;

then A11: 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 A7, FUNCT_4:13

.= I . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A10, AFINSQ_1:def 3

.= (I ';' J) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A10, AFINSQ_1:def 3

.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A11, FUNCT_4:13

.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by A5, A9, NAT_1:13, PBOOLE:143 ;

hence Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(m + 1)) by A5, A9, A8, A6, NAT_1:13; :: thesis: verum

end;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

A6: 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))) ;

A7: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom (stop I) by A1, SCMPDS_6:def 2;

A8: 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 A9: 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 A10: IC (Comput ((P +* (stop I)),(Initialize s),m)) in dom I by A1, A2, SCMPDS_6:26;

then A11: 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 A7, FUNCT_4:13

.= I . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A10, AFINSQ_1:def 3

.= (I ';' J) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A10, AFINSQ_1:def 3

.= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),(Initialize s),m))) by A11, FUNCT_4:13

.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(Initialize s),m))) by A5, A9, NAT_1:13, PBOOLE:143 ;

hence Comput ((P +* (stop I)),(Initialize s),(m + 1)) = Comput ((P +* (I ';' J)),(Initialize s),(m + 1)) by A5, A9, A8, A6, NAT_1:13; :: thesis: verum

for k being Nat holds S

hence Comput ((P +* (stop I)),(Initialize s),k) = Comput ((P +* (I ';' J)),(Initialize s),k) by A3; :: thesis: verum