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 c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of

for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

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

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

let k be Nat; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k) )

set m = LifeSpan ((P +* (stop I)),(Initialize s));

assume that

A1: I c= J and

A2: I is_closed_on s,P and

A3: I is_halting_on s,P and

A4: k <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

set s1 = Initialize s;

set s2 = Initialize s;

set P1 = P +* J;

set P2 = P +* (stop I);

defpred S_{1}[ Nat] means ( $1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),$1) = Comput ((P +* (stop I)),(Initialize s),$1) );

_{1}[ 0 ]
;

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

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

for I, J being Program of

for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of

for k being Nat st I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

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

Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

let k be Nat; :: thesis: ( I c= J & I is_closed_on s,P & I is_halting_on s,P & k <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k) )

set m = LifeSpan ((P +* (stop I)),(Initialize s));

assume that

A1: I c= J and

A2: I is_closed_on s,P and

A3: I is_halting_on s,P and

A4: k <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),k) = Comput ((P +* (stop I)),(Initialize s),k)

set s1 = Initialize s;

set s2 = Initialize s;

set P1 = P +* J;

set P2 = P +* (stop I);

defpred S

A5: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A15:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A6: S

now :: thesis: ( k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) implies Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1)) )

hence
SA7: Comput ((P +* (stop I)),(Initialize s),(k + 1)) =
Following ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k)))
by EXTPRO_1:3

.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k)))),(Comput ((P +* (stop I)),(Initialize s),k))) ;

A8: Comput ((P +* J),(Initialize s),(k + 1)) = Following ((P +* J),(Comput ((P +* J),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k)))),(Comput ((P +* J),(Initialize s),k))) ;

A9: k < k + 1 by XREAL_1:29;

assume A10: k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1))

then k < LifeSpan ((P +* (stop I)),(Initialize s)) by A9, XXREAL_0:2;

then A11: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by A2, A3, SCMPDS_6:26;

then A12: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by FUNCT_4:12;

A13: J c= P +* J by FUNCT_4:25;

A14: dom I c= dom J by A1, RELAT_1:11;

CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k))) = (P +* J) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A6, A10, A9, PBOOLE:143, XXREAL_0:2

.= J . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A13, A14, A11, GRFUNC_1:2

.= I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A1, A11, GRFUNC_1:2

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

.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A12, FUNCT_4:13

.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:143 ;

hence Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1)) by A6, A10, A9, A8, A7, XXREAL_0:2; :: thesis: verum

end;.= Exec ((CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k)))),(Comput ((P +* (stop I)),(Initialize s),k))) ;

A8: Comput ((P +* J),(Initialize s),(k + 1)) = Following ((P +* J),(Comput ((P +* J),(Initialize s),k))) by EXTPRO_1:3

.= Exec ((CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k)))),(Comput ((P +* J),(Initialize s),k))) ;

A9: k < k + 1 by XREAL_1:29;

assume A10: k + 1 <= LifeSpan ((P +* (stop I)),(Initialize s)) ; :: thesis: Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1))

then k < LifeSpan ((P +* (stop I)),(Initialize s)) by A9, XXREAL_0:2;

then A11: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I by A2, A3, SCMPDS_6:26;

then A12: IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by FUNCT_4:12;

A13: J c= P +* J by FUNCT_4:25;

A14: dom I c= dom J by A1, RELAT_1:11;

CurInstr ((P +* J),(Comput ((P +* J),(Initialize s),k))) = (P +* J) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A6, A10, A9, PBOOLE:143, XXREAL_0:2

.= J . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A13, A14, A11, GRFUNC_1:2

.= I . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A1, A11, GRFUNC_1:2

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

.= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),k))) by A12, FUNCT_4:13

.= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) by PBOOLE:143 ;

hence Comput ((P +* J),(Initialize s),(k + 1)) = Comput ((P +* (stop I)),(Initialize s),(k + 1)) by A6, A10, A9, A8, A7, XXREAL_0:2; :: thesis: verum

for k being Nat holds S

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