let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being parahalting Program of

for J being Program of

for k being 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

for J being Program of

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

for k being 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 ; :: thesis: for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds

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

let k be 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);

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

A1: for n being Nat st S_{1}[n] holds

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

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

hence ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) ) ; :: thesis: verum

for I being parahalting Program of

for J being Program of

for k being 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

for J being Program of

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

for k being 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 ; :: thesis: for k being Nat st k <= LifeSpan ((P +* (stop I)),s) holds

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

let k be 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);

defpred S

A1: for n being Nat st S

S

proof

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

assume A2: ( m <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,m) = Comput ((P +* (I ';' J)),s,m) ) ; :: thesis: S_{1}[m + 1]

A3: 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 A4: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by SCMPDS_4:def 6;

A5: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3;

assume A6: m + 1 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1))

A7: m < LifeSpan ((P +* (stop I)),s) by A6, NAT_1:13;

then IC (Comput ((P +* (stop I)),s,m)) in dom I by Th12;

then A8: IC (Comput ((P +* (stop I)),s,m)) in dom (I ';' J) by FUNCT_4:12;

A9: IC (Comput ((P +* (stop I)),s,m)) in dom I by A7, Th12;

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 A4, FUNCT_4:13

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

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

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

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

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

end;assume A2: ( m <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,m) = Comput ((P +* (I ';' J)),s,m) ) ; :: thesis: S

A3: 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 A4: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by SCMPDS_4:def 6;

A5: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3;

assume A6: m + 1 <= LifeSpan ((P +* (stop I)),s) ; :: thesis: Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1))

A7: m < LifeSpan ((P +* (stop I)),s) by A6, NAT_1:13;

then IC (Comput ((P +* (stop I)),s,m)) in dom I by Th12;

then A8: IC (Comput ((P +* (stop I)),s,m)) in dom (I ';' J) by FUNCT_4:12;

A9: IC (Comput ((P +* (stop I)),s,m)) in dom I by A7, Th12;

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 A4, FUNCT_4:13

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

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

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

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

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

for k being Nat holds S

hence ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) ) ; :: thesis: verum