:: The Construction and Computation of While-loop Programs for SCMPDS
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

set A = NAT ;

set D = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_8:1

for a being Int_position ex i being Element of NAT st a = intpos i

proof end;

definition

let t be State of SCMPDS;
func Dstate t -> State of SCMPDS means :Def1: :: SCMPDS_8:def 1
for x being set holds
( ( x in SCM-Data-Loc implies it . x = t . x ) & ( x in NAT implies it . x = goto 0 ) & ( x = IC implies it . x = 0 ) );
existence
ex b₁ being State of SCMPDS st
for x being set holds
( ( x in SCM-Data-Loc implies b₁ . x = t . x ) & ( x in NAT implies b₁ . x = goto 0 ) & ( x = IC implies b₁ . x = 0 ) )

proof end;

uniqueness
for b₁, b₂ being State of SCMPDS st ( for x being set holds
( ( x in SCM-Data-Loc implies b₁ . x = t . x ) & ( x in NAT implies b₁ . x = goto 0 ) & ( x = IC implies b₁ . x = 0 ) ) ) & ( for x being set holds
( ( x in SCM-Data-Loc implies b₂ . x = t . x ) & ( x in NAT implies b₂ . x = goto 0 ) & ( x = IC implies b₂ . x = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Dstate SCMPDS_8:def 1 :
for t, b₂ being State of SCMPDS holds
( b₂ = Dstate t iff for x being set holds
( ( x in SCM-Data-Loc implies b₂ . x = t . x ) & ( x in NAT implies b₂ . x = goto 0 ) & ( x = IC implies b₂ . x = 0 ) ) );

theorem Th2: :: SCMPDS_8:2

for t1, t2 being State of SCMPDS st DataPart t1 = DataPart t2 holds
Dstate t1 = Dstate t2

proof end;

theorem Th3: :: SCMPDS_8:3

for t being State of SCMPDS
for i being Instruction of SCMPDS st InsCode i in {0,4,5,6} holds
Dstate t = Dstate (Exec (i,t))

proof end;

theorem Th4: :: SCMPDS_8:4

for a being Int_position
for s being State of SCMPDS holds (Dstate s) . a = s . a

proof end;

theorem Th5: :: SCMPDS_8:5

for a being Int_position ex f being Function of (product the Object-Kind of SCMPDS),NAT st
for s being State of SCMPDS holds
( ( s . a <= 0 implies f . s = 0 ) & ( s . a > 0 implies f . s = s . a ) )

proof end;

begin

definition

let a be Int_position ;
let i be Integer;
let I be Program of SCMPDS;
func while<0 (a,i,I) -> Program of SCMPDS equals :: SCMPDS_8:def 2
(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));
coherence
(((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

end;

:: deftheorem defines while<0 SCMPDS_8:def 2 :
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds while<0 (a,i,I) = (((a,i) >=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

registration

let I be shiftable Program of SCMPDS;
let a be Int_position ;
let i be Integer;
cluster while<0 (a,i,I) -> shiftable ;
correctness
coherence
while<0 (a,i,I) is shiftable ;

proof end;

end;

registration

let I be halt-free Program of SCMPDS;
let a be Int_position ;
let i be Integer;
cluster while<0 (a,i,I) -> halt-free ;
correctness
coherence
while<0 (a,i,I) is halt-free ;
;

end;

theorem Th6: :: SCMPDS_8:6

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (while<0 (a,i,I)) = (card I) + 2

proof end;

Lm1: for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (stop (while<0 (a,i,I))) = (card I) + 3

proof end;

theorem Th7: :: SCMPDS_8:7

for a being Int_position
for i being Integer
for m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while<0 (a,i,I)) )

proof end;

theorem Th8: :: SCMPDS_8:8

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( (while<0 (a,i,I)) . 0 = (a,i) >=0_goto ((card I) + 2) & (while<0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

proof end;

theorem Th9: :: SCMPDS_8:9

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th10: :: SCMPDS_8:10

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a, c being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds
IExec ((while<0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem :: SCMPDS_8:11

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds
IC (IExec ((while<0 (a,i,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_8:12

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a, b being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds
(IExec ((while<0 (a,i,I)),P,s)) . b = s . b

proof end;

Lm2: for I being Program of SCMPDS
for a being Int_position
for i being Integer holds Shift (I,1) c= while<0 (a,i,I)

proof end;

scheme :: SCMPDS_8:sch 1
WhileLHalt{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ State of SCMPDS] } :

( ( F₁(F₂()) = F₁(F₂()) or P₁[F₂()] ) & while<0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() )

provided

A2: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) < 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

scheme :: SCMPDS_8:sch 2
WhileLExec{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ State of SCMPDS] } :

( ( F₁(F₂()) = F₁(F₂()) or P₁[F₂()] ) & IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),F₂()) = IExec ((while<0 (F₅(),F₆(),F₄())),F₃(),(IExec (F₄(),F₃(),F₂()))) )

provided

A2: F₂() . (DataLoc ((F₂() . F₅()),F₆())) < 0 and
A3: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) >= 0 and
A4: P₁[ Dstate F₂()] and
A5: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) < 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

theorem :: SCMPDS_8:13

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem :: SCMPDS_8:14

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st s . (DataLoc ((s . a),i)) < 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) >= 0 ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(IExec (I,P,s)))

proof end;

theorem Th15: :: SCMPDS_8:15

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )

proof end;

theorem :: SCMPDS_8:16

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),P,s) = IExec ((while<0 (a,i,I)),P,(IExec (I,P,s)))

proof end;

begin

definition

let a be Int_position ;
let i be Integer;
let I be Program of SCMPDS;
func while>0 (a,i,I) -> Program of SCMPDS equals :: SCMPDS_8:def 3
(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));
coherence
(((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1))) is Program of SCMPDS ;

end;

:: deftheorem defines while>0 SCMPDS_8:def 3 :
for a being Int_position
for i being Integer
for I being Program of SCMPDS holds while>0 (a,i,I) = (((a,i) <=0_goto ((card I) + 2)) ';' I) ';' (goto (- ((card I) + 1)));

registration

let I be shiftable Program of SCMPDS;
let a be Int_position ;
let i be Integer;
cluster while>0 (a,i,I) -> shiftable ;
correctness
coherence
while>0 (a,i,I) is shiftable ;

proof end;

end;

registration

let I be halt-free Program of SCMPDS;
let a be Int_position ;
let i be Integer;
cluster while>0 (a,i,I) -> halt-free ;
correctness
coherence
while>0 (a,i,I) is halt-free ;
;

end;

theorem Th17: :: SCMPDS_8:17

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (while>0 (a,i,I)) = (card I) + 2

proof end;

Lm3: for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (stop (while>0 (a,i,I))) = (card I) + 3

proof end;

theorem Th18: :: SCMPDS_8:18

for a being Int_position
for i being Integer
for m being Element of NAT
for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )

proof end;

theorem Th19: :: SCMPDS_8:19

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( (while>0 (a,i,I)) . 0 = (a,i) <=0_goto ((card I) + 2) & (while>0 (a,i,I)) . ((card I) + 1) = goto (- ((card I) + 1)) )

proof end;

theorem Th20: :: SCMPDS_8:20

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th21: :: SCMPDS_8:21

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a, c being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds
IExec ((while>0 (a,i,I)),P,s) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem :: SCMPDS_8:22

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds
IC (IExec ((while>0 (a,i,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_8:23

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being Program of SCMPDS
for a, b being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) <= 0 holds
(IExec ((while>0 (a,i,I)),P,s)) . b = s . b

proof end;

Lm4: for I being Program of SCMPDS
for a being Int_position
for i being Integer holds Shift (I,1) c= while>0 (a,i,I)

proof end;

scheme :: SCMPDS_8:sch 3
WhileGHalt{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ State of SCMPDS] } :

( ( F₁(F₂()) = F₁(F₂()) or P₁[F₂()] ) & while>0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while>0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() )

provided

A2: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) <= 0 and
A3: P₁[ Dstate F₂()] and
A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) > 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

scheme :: SCMPDS_8:sch 4
WhileGExec{ F₁( State of SCMPDS) -> Element of NAT , F₂() -> State of SCMPDS, F₃() -> the Instructions of SCMPDS -valued ManySortedSet of NAT , F₄() -> halt-free shiftable Program of SCMPDS, F₅() -> Int_position , F₆() -> Integer, P₁[ State of SCMPDS] } :

( ( F₁(F₂()) = F₁(F₂()) or P₁[F₂()] ) & IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),F₂()) = IExec ((while>0 (F₅(),F₆(),F₄())),F₃(),(IExec (F₄(),F₃(),F₂()))) )

provided

A2: F₂() . (DataLoc ((F₂() . F₅()),F₆())) > 0 and
A3: for t being State of SCMPDS st P₁[ Dstate t] & F₁((Dstate t)) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) <= 0 and
A4: P₁[ Dstate F₂()] and
A5: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) > 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & F₁((Dstate (IExec (F₄(),Q,t)))) < F₁((Dstate t)) & P₁[ Dstate (IExec (F₄(),Q,t))] )

proof end;

theorem Th24: :: SCMPDS_8:24

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X, Y being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P )

proof end;

theorem Th25: :: SCMPDS_8:25

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X, Y being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st s . (DataLoc ((s . a),i)) > 0 & card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s)))

proof end;

theorem :: SCMPDS_8:26

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set
for f being Function of (product the Object-Kind of SCMPDS),NAT st card I > 0 & ( for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )

proof end;

theorem Th27: :: SCMPDS_8:27

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X, Y being set st ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )

proof end;

theorem :: SCMPDS_8:28

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )

proof end;

theorem :: SCMPDS_8:29

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for X being set st card I > 0 & ( for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(IExec (I,P,s))) ) )

proof end;