:: SCMPDS_8 semantic presentation

set c1 = the Instruction-Locations of SCMPDS ;

set c2 = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_8:1
for b1 being Int_position ex b2 being Nat st b1 = intpos b2
proof end;

definition
let c3 be State of SCMPDS ;
func Dstate c1 -> State of SCMPDS means :Def1: :: SCMPDS_8:def 1
for b1 being set holds
( ( b1 in SCM-Data-Loc implies a2 . b1 = a1 . b1 ) & ( b1 in the Instruction-Locations of SCMPDS implies a2 . b1 = goto 0 ) & ( b1 = IC SCMPDS implies a2 . b1 = inspos 0 ) );
existence
ex b1 being State of SCMPDS st
for b2 being set holds
( ( b2 in SCM-Data-Loc implies b1 . b2 = c3 . b2 ) & ( b2 in the Instruction-Locations of SCMPDS implies b1 . b2 = goto 0 ) & ( b2 = IC SCMPDS implies b1 . b2 = inspos 0 ) )
proof end;
uniqueness
for b1, b2 being State of SCMPDS st ( for b3 being set holds
( ( b3 in SCM-Data-Loc implies b1 . b3 = c3 . b3 ) & ( b3 in the Instruction-Locations of SCMPDS implies b1 . b3 = goto 0 ) & ( b3 = IC SCMPDS implies b1 . b3 = inspos 0 ) ) ) & ( for b3 being set holds
( ( b3 in SCM-Data-Loc implies b2 . b3 = c3 . b3 ) & ( b3 in the Instruction-Locations of SCMPDS implies b2 . b3 = goto 0 ) & ( b3 = IC SCMPDS implies b2 . b3 = inspos 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Dstate SCMPDS_8:def 1 :
for b1, b2 being State of SCMPDS holds
( b2 = Dstate b1 iff for b3 being set holds
( ( b3 in SCM-Data-Loc implies b2 . b3 = b1 . b3 ) & ( b3 in the Instruction-Locations of SCMPDS implies b2 . b3 = goto 0 ) & ( b3 = IC SCMPDS implies b2 . b3 = inspos 0 ) ) );

theorem Th2: :: SCMPDS_8:2
for b1, b2 being State of SCMPDS st b1 | SCM-Data-Loc = b2 | SCM-Data-Loc holds
Dstate b1 = Dstate b2
proof end;

theorem Th3: :: SCMPDS_8:3
for b1 being State of SCMPDS
for b2 being Instruction of SCMPDS st InsCode b2 in {0,4,5,6} holds
Dstate b1 = Dstate (Exec b2,b1)
proof end;

theorem Th4: :: SCMPDS_8:4
for b1 being Int_position
for b2 being State of SCMPDS holds (Dstate b2) . b1 = b2 . b1
proof end;

theorem Th5: :: SCMPDS_8:5
for b1 being Int_position ex b2 being Function of product the Object-Kind of SCMPDS , NAT st
for b3 being State of SCMPDS holds
( ( b3 . b1 <= 0 implies b2 . b3 = 0 ) & ( b3 . b1 > 0 implies b2 . b3 = b3 . b1 ) )
proof end;

definition
let c3 be Int_position ;
let c4 be Integer;
let c5 be Program-block;
func while<0 c1,c2,c3 -> Program-block equals :: SCMPDS_8:def 2
((a1,a2 >=0_goto ((card a3) + 2)) ';' a3) ';' (goto (- ((card a3) + 1)));
coherence
((c3,c4 >=0_goto ((card c5) + 2)) ';' c5) ';' (goto (- ((card c5) + 1))) is Program-block ;
end;

:: deftheorem Def2 defines while<0 SCMPDS_8:def 2 :
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds while<0 b1,b2,b3 = ((b1,b2 >=0_goto ((card b3) + 2)) ';' b3) ';' (goto (- ((card b3) + 1)));

registration
let c3 be shiftable Program-block;
let c4 be Int_position ;
let c5 be Integer;
cluster while<0 a2,a3,a1 -> shiftable ;
correctness
coherence
while<0 c4,c5,c3 is shiftable;
proof end;
end;

registration
let c3 be No-StopCode Program-block;
let c4 be Int_position ;
let c5 be Integer;
cluster while<0 a2,a3,a1 -> No-StopCode ;
correctness
coherence
while<0 c4,c5,c3 is No-StopCode;
;
end;

theorem Th6: :: SCMPDS_8:6
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds card (while<0 b1,b2,b3) = (card b3) + 2
proof end;

Lemma8: for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds card (stop (while<0 b1,b2,b3)) = (card b3) + 3
proof end;

theorem Th7: :: SCMPDS_8:7
for b1 being Int_position
for b2 being Integer
for b3 being Nat
for b4 being Program-block holds
( b3 < (card b4) + 2 iff inspos b3 in dom (while<0 b1,b2,b4) )
proof end;

theorem Th8: :: SCMPDS_8:8
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds
( (while<0 b1,b2,b3) . (inspos 0) = b1,b2 >=0_goto ((card b3) + 2) & (while<0 b1,b2,b3) . (inspos ((card b3) + 1)) = goto (- ((card b3) + 1)) )
proof end;

Lemma11: for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds while<0 b1,b2,b3 = (b1,b2 >=0_goto ((card b3) + 2)) ';' (b3 ';' (goto (- ((card b3) + 1))))
by SCMPDS_4:51;

theorem Th9: :: SCMPDS_8:9
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being Int_position
for b4 being Integer st b1 . (DataLoc (b1 . b3),b4) >= 0 holds
( while<0 b3,b4,b2 is_closed_on b1 & while<0 b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th10: :: SCMPDS_8:10
for b1 being State of SCMPDS
for b2 being Program-block
for b3, b4 being Int_position
for b5 being Integer st b1 . (DataLoc (b1 . b3),b5) >= 0 holds
IExec (while<0 b3,b5,b2),b1 = b1 +* (Start-At (inspos ((card b2) + 2)))
proof end;

theorem Th11: :: SCMPDS_8:11
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being Int_position
for b4 being Integer st b1 . (DataLoc (b1 . b3),b4) >= 0 holds
IC (IExec (while<0 b3,b4,b2),b1) = inspos ((card b2) + 2)
proof end;

theorem Th12: :: SCMPDS_8:12
for b1 being State of SCMPDS
for b2 being Program-block
for b3, b4 being Int_position
for b5 being Integer st b1 . (DataLoc (b1 . b3),b5) >= 0 holds
(IExec (while<0 b3,b5,b2),b1) . b4 = b1 . b4
proof end;

Lemma14: for b1 being Program-block
for b2 being Int_position
for b3 being Integer holds Shift b1,1 c= while<0 b2,b3,b1
proof end;

scheme :: SCMPDS_8:sch 1
s1{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ State of SCMPDS ] } :
( ( F1(F2()) = F1(F2()) or P1[F2()] ) & while<0 F4(),F5(),F3() is_closed_on F2() & while<0 F4(),F5(),F3() is_halting_on F2() )
provided
E15: card F3() > 0 and
E16: for b1 being State of SCMPDS st P1[ Dstate b1] & F1((Dstate b1)) = 0 holds
b1 . (DataLoc (F2() . F4()),F5()) >= 0 and
E17: P1[ Dstate F2()] and
E18: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F4() = F2() . F4() & b1 . (DataLoc (F2() . F4()),F5()) < 0 holds
( (IExec F3(),b1) . F4() = b1 . F4() & F3() is_closed_on b1 & F3() is_halting_on b1 & F1((Dstate (IExec F3(),b1))) < F1((Dstate b1)) & P1[ Dstate (IExec F3(),b1)] )
proof end;

scheme :: SCMPDS_8:sch 2
s2{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ State of SCMPDS ] } :
( ( F1(F2()) = F1(F2()) or P1[F2()] ) & IExec (while<0 F4(),F5(),F3()),F2() = IExec (while<0 F4(),F5(),F3()),(IExec F3(),F2()) )
provided
E15: card F3() > 0 and
E16: F2() . (DataLoc (F2() . F4()),F5()) < 0 and
E17: for b1 being State of SCMPDS st P1[ Dstate b1] & F1((Dstate b1)) = 0 holds
b1 . (DataLoc (F2() . F4()),F5()) >= 0 and
E18: P1[ Dstate F2()] and
E19: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F4() = F2() . F4() & b1 . (DataLoc (F2() . F4()),F5()) < 0 holds
( (IExec F3(),b1) . F4() = b1 . F4() & F3() is_closed_on b1 & F3() is_halting_on b1 & F1((Dstate (IExec F3(),b1))) < F1((Dstate b1)) & P1[ Dstate (IExec F3(),b1)] )
proof end;

theorem Th13: :: SCMPDS_8:13
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set
for b6 being Function of product the Object-Kind of SCMPDS , NAT st card b2 > 0 & ( for b7 being State of SCMPDS st b6 . (Dstate b7) = 0 holds
b7 . (DataLoc (b1 . b3),b4) >= 0 ) & ( for b7 being State of SCMPDS st ( for b8 being Int_position st b8 in b5 holds
b7 . b8 = b1 . b8 ) & b7 . b3 = b1 . b3 & b7 . (DataLoc (b1 . b3),b4) < 0 holds
( (IExec b2,b7) . b3 = b7 . b3 & b6 . (Dstate (IExec b2,b7)) < b6 . (Dstate b7) & b2 is_closed_on b7 & b2 is_halting_on b7 & ( for b8 being Int_position st b8 in b5 holds
(IExec b2,b7) . b8 = b7 . b8 ) ) ) holds
( while<0 b3,b4,b2 is_closed_on b1 & while<0 b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th14: :: SCMPDS_8:14
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set
for b6 being Function of product the Object-Kind of SCMPDS , NAT st card b2 > 0 & b1 . (DataLoc (b1 . b3),b4) < 0 & ( for b7 being State of SCMPDS st b6 . (Dstate b7) = 0 holds
b7 . (DataLoc (b1 . b3),b4) >= 0 ) & ( for b7 being State of SCMPDS st ( for b8 being Int_position st b8 in b5 holds
b7 . b8 = b1 . b8 ) & b7 . b3 = b1 . b3 & b7 . (DataLoc (b1 . b3),b4) < 0 holds
( (IExec b2,b7) . b3 = b7 . b3 & b2 is_closed_on b7 & b2 is_halting_on b7 & b6 . (Dstate (IExec b2,b7)) < b6 . (Dstate b7) & ( for b8 being Int_position st b8 in b5 holds
(IExec b2,b7) . b8 = b7 . b8 ) ) ) holds
IExec (while<0 b3,b4,b2),b1 = IExec (while<0 b3,b4,b2),(IExec b2,b1)
proof end;

theorem Th15: :: SCMPDS_8:15
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set st card b2 > 0 & ( for b6 being State of SCMPDS st ( for b7 being Int_position st b7 in b5 holds
b6 . b7 = b1 . b7 ) & b6 . b3 = b1 . b3 & b6 . (DataLoc (b1 . b3),b4) < 0 holds
( (IExec b2,b6) . b3 = b6 . b3 & (IExec b2,b6) . (DataLoc (b1 . b3),b4) > b6 . (DataLoc (b1 . b3),b4) & b2 is_closed_on b6 & b2 is_halting_on b6 & ( for b7 being Int_position st b7 in b5 holds
(IExec b2,b6) . b7 = b6 . b7 ) ) ) holds
( while<0 b3,b4,b2 is_closed_on b1 & while<0 b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th16: :: SCMPDS_8:16
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set st b1 . (DataLoc (b1 . b3),b4) < 0 & card b2 > 0 & ( for b6 being State of SCMPDS st ( for b7 being Int_position st b7 in b5 holds
b6 . b7 = b1 . b7 ) & b6 . b3 = b1 . b3 & b6 . (DataLoc (b1 . b3),b4) < 0 holds
( (IExec b2,b6) . b3 = b6 . b3 & (IExec b2,b6) . (DataLoc (b1 . b3),b4) > b6 . (DataLoc (b1 . b3),b4) & b2 is_closed_on b6 & b2 is_halting_on b6 & ( for b7 being Int_position st b7 in b5 holds
(IExec b2,b6) . b7 = b6 . b7 ) ) ) holds
IExec (while<0 b3,b4,b2),b1 = IExec (while<0 b3,b4,b2),(IExec b2,b1)
proof end;

definition
let c3 be Int_position ;
let c4 be Integer;
let c5 be Program-block;
func while>0 c1,c2,c3 -> Program-block equals :: SCMPDS_8:def 3
((a1,a2 <=0_goto ((card a3) + 2)) ';' a3) ';' (goto (- ((card a3) + 1)));
coherence
((c3,c4 <=0_goto ((card c5) + 2)) ';' c5) ';' (goto (- ((card c5) + 1))) is Program-block ;
end;

:: deftheorem Def3 defines while>0 SCMPDS_8:def 3 :
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds while>0 b1,b2,b3 = ((b1,b2 <=0_goto ((card b3) + 2)) ';' b3) ';' (goto (- ((card b3) + 1)));

registration
let c3 be shiftable Program-block;
let c4 be Int_position ;
let c5 be Integer;
cluster while>0 a2,a3,a1 -> shiftable ;
correctness
coherence
while>0 c4,c5,c3 is shiftable;
proof end;
end;

registration
let c3 be No-StopCode Program-block;
let c4 be Int_position ;
let c5 be Integer;
cluster while>0 a2,a3,a1 -> No-StopCode ;
correctness
coherence
while>0 c4,c5,c3 is No-StopCode;
;
end;

theorem Th17: :: SCMPDS_8:17
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds card (while>0 b1,b2,b3) = (card b3) + 2
proof end;

Lemma17: for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds card (stop (while>0 b1,b2,b3)) = (card b3) + 3
proof end;

theorem Th18: :: SCMPDS_8:18
for b1 being Int_position
for b2 being Integer
for b3 being Nat
for b4 being Program-block holds
( b3 < (card b4) + 2 iff inspos b3 in dom (while>0 b1,b2,b4) )
proof end;

theorem Th19: :: SCMPDS_8:19
for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds
( (while>0 b1,b2,b3) . (inspos 0) = b1,b2 <=0_goto ((card b3) + 2) & (while>0 b1,b2,b3) . (inspos ((card b3) + 1)) = goto (- ((card b3) + 1)) )
proof end;

Lemma20: for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds while>0 b1,b2,b3 = (b1,b2 <=0_goto ((card b3) + 2)) ';' (b3 ';' (goto (- ((card b3) + 1))))
by SCMPDS_4:51;

theorem Th20: :: SCMPDS_8:20
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being Int_position
for b4 being Integer st b1 . (DataLoc (b1 . b3),b4) <= 0 holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th21: :: SCMPDS_8:21
for b1 being State of SCMPDS
for b2 being Program-block
for b3, b4 being Int_position
for b5 being Integer st b1 . (DataLoc (b1 . b3),b5) <= 0 holds
IExec (while>0 b3,b5,b2),b1 = b1 +* (Start-At (inspos ((card b2) + 2)))
proof end;

theorem Th22: :: SCMPDS_8:22
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being Int_position
for b4 being Integer st b1 . (DataLoc (b1 . b3),b4) <= 0 holds
IC (IExec (while>0 b3,b4,b2),b1) = inspos ((card b2) + 2)
proof end;

theorem Th23: :: SCMPDS_8:23
for b1 being State of SCMPDS
for b2 being Program-block
for b3, b4 being Int_position
for b5 being Integer st b1 . (DataLoc (b1 . b3),b5) <= 0 holds
(IExec (while>0 b3,b5,b2),b1) . b4 = b1 . b4
proof end;

Lemma23: for b1 being Program-block
for b2 being Int_position
for b3 being Integer holds Shift b1,1 c= while>0 b2,b3,b1
proof end;

scheme :: SCMPDS_8:sch 3
s3{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ State of SCMPDS ] } :
( ( F1(F2()) = F1(F2()) or P1[F2()] ) & while>0 F4(),F5(),F3() is_closed_on F2() & while>0 F4(),F5(),F3() is_halting_on F2() )
provided
E24: card F3() > 0 and
E25: for b1 being State of SCMPDS st P1[ Dstate b1] & F1((Dstate b1)) = 0 holds
b1 . (DataLoc (F2() . F4()),F5()) <= 0 and
E26: P1[ Dstate F2()] and
E27: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F4() = F2() . F4() & b1 . (DataLoc (F2() . F4()),F5()) > 0 holds
( (IExec F3(),b1) . F4() = b1 . F4() & F3() is_closed_on b1 & F3() is_halting_on b1 & F1((Dstate (IExec F3(),b1))) < F1((Dstate b1)) & P1[ Dstate (IExec F3(),b1)] )
proof end;

scheme :: SCMPDS_8:sch 4
s4{ F1( State of SCMPDS ) -> Nat, F2() -> State of SCMPDS , F3() -> shiftable No-StopCode Program-block, F4() -> Int_position , F5() -> Integer, P1[ State of SCMPDS ] } :
( ( F1(F2()) = F1(F2()) or P1[F2()] ) & IExec (while>0 F4(),F5(),F3()),F2() = IExec (while>0 F4(),F5(),F3()),(IExec F3(),F2()) )
provided
E24: card F3() > 0 and
E25: F2() . (DataLoc (F2() . F4()),F5()) > 0 and
E26: for b1 being State of SCMPDS st P1[ Dstate b1] & F1((Dstate b1)) = 0 holds
b1 . (DataLoc (F2() . F4()),F5()) <= 0 and
E27: P1[ Dstate F2()] and
E28: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F4() = F2() . F4() & b1 . (DataLoc (F2() . F4()),F5()) > 0 holds
( (IExec F3(),b1) . F4() = b1 . F4() & F3() is_closed_on b1 & F3() is_halting_on b1 & F1((Dstate (IExec F3(),b1))) < F1((Dstate b1)) & P1[ Dstate (IExec F3(),b1)] )
proof end;

theorem Th24: :: SCMPDS_8:24
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7 being set
for b8 being Function of product the Object-Kind of SCMPDS , NAT st card b2 > 0 & ( for b9 being State of SCMPDS st b8 . (Dstate b9) = 0 holds
b9 . (DataLoc (b1 . b3),b4) <= 0 ) & ( for b9 being Int_position st b9 in b6 holds
b1 . b9 >= b5 + (b1 . (DataLoc (b1 . b3),b4)) ) & ( for b9 being State of SCMPDS st ( for b10 being Int_position st b10 in b6 holds
b9 . b10 >= b5 + (b9 . (DataLoc (b1 . b3),b4)) ) & ( for b10 being Int_position st b10 in b7 holds
b9 . b10 = b1 . b10 ) & b9 . b3 = b1 . b3 & b9 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b9) . b3 = b9 . b3 & b2 is_closed_on b9 & b2 is_halting_on b9 & b8 . (Dstate (IExec b2,b9)) < b8 . (Dstate b9) & ( for b10 being Int_position st b10 in b6 holds
(IExec b2,b9) . b10 >= b5 + ((IExec b2,b9) . (DataLoc (b1 . b3),b4)) ) & ( for b10 being Int_position st b10 in b7 holds
(IExec b2,b9) . b10 = b9 . b10 ) ) ) holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 )
proof end;

theorem Th25: :: SCMPDS_8:25
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7 being set
for b8 being Function of product the Object-Kind of SCMPDS , NAT st b1 . (DataLoc (b1 . b3),b4) > 0 & card b2 > 0 & ( for b9 being State of SCMPDS st b8 . (Dstate b9) = 0 holds
b9 . (DataLoc (b1 . b3),b4) <= 0 ) & ( for b9 being Int_position st b9 in b6 holds
b1 . b9 >= b5 + (b1 . (DataLoc (b1 . b3),b4)) ) & ( for b9 being State of SCMPDS st ( for b10 being Int_position st b10 in b6 holds
b9 . b10 >= b5 + (b9 . (DataLoc (b1 . b3),b4)) ) & ( for b10 being Int_position st b10 in b7 holds
b9 . b10 = b1 . b10 ) & b9 . b3 = b1 . b3 & b9 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b9) . b3 = b9 . b3 & b2 is_closed_on b9 & b2 is_halting_on b9 & b8 . (Dstate (IExec b2,b9)) < b8 . (Dstate b9) & ( for b10 being Int_position st b10 in b6 holds
(IExec b2,b9) . b10 >= b5 + ((IExec b2,b9) . (DataLoc (b1 . b3),b4)) ) & ( for b10 being Int_position st b10 in b7 holds
(IExec b2,b9) . b10 = b9 . b10 ) ) ) holds
IExec (while>0 b3,b4,b2),b1 = IExec (while>0 b3,b4,b2),(IExec b2,b1)
proof end;

theorem Th26: :: SCMPDS_8:26
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set
for b6 being Function of product the Object-Kind of SCMPDS , NAT st card b2 > 0 & ( for b7 being State of SCMPDS st b6 . (Dstate b7) = 0 holds
b7 . (DataLoc (b1 . b3),b4) <= 0 ) & ( for b7 being State of SCMPDS st ( for b8 being Int_position st b8 in b5 holds
b7 . b8 = b1 . b8 ) & b7 . b3 = b1 . b3 & b7 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b7) . b3 = b7 . b3 & b2 is_closed_on b7 & b2 is_halting_on b7 & b6 . (Dstate (IExec b2,b7)) < b6 . (Dstate b7) & ( for b8 being Int_position st b8 in b5 holds
(IExec b2,b7) . b8 = b7 . b8 ) ) ) holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b4) > 0 implies IExec (while>0 b3,b4,b2),b1 = IExec (while>0 b3,b4,b2),(IExec b2,b1) ) )
proof end;

theorem Th27: :: SCMPDS_8:27
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7 being set st card b2 > 0 & ( for b8 being Int_position st b8 in b6 holds
b1 . b8 >= b5 + (b1 . (DataLoc (b1 . b3),b4)) ) & ( for b8 being State of SCMPDS st ( for b9 being Int_position st b9 in b6 holds
b8 . b9 >= b5 + (b8 . (DataLoc (b1 . b3),b4)) ) & ( for b9 being Int_position st b9 in b7 holds
b8 . b9 = b1 . b9 ) & b8 . b3 = b1 . b3 & b8 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b8) . b3 = b8 . b3 & b2 is_closed_on b8 & b2 is_halting_on b8 & (IExec b2,b8) . (DataLoc (b1 . b3),b4) < b8 . (DataLoc (b1 . b3),b4) & ( for b9 being Int_position st b9 in b6 holds
(IExec b2,b8) . b9 >= b5 + ((IExec b2,b8) . (DataLoc (b1 . b3),b4)) ) & ( for b9 being Int_position st b9 in b7 holds
(IExec b2,b8) . b9 = b8 . b9 ) ) ) holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b4) > 0 implies IExec (while>0 b3,b4,b2),b1 = IExec (while>0 b3,b4,b2),(IExec b2,b1) ) )
proof end;

theorem Th28: :: SCMPDS_8:28
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being set st card b2 > 0 & ( for b6 being State of SCMPDS st ( for b7 being Int_position st b7 in b5 holds
b6 . b7 = b1 . b7 ) & b6 . b3 = b1 . b3 & b6 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b6) . b3 = b6 . b3 & b2 is_closed_on b6 & b2 is_halting_on b6 & (IExec b2,b6) . (DataLoc (b1 . b3),b4) < b6 . (DataLoc (b1 . b3),b4) & ( for b7 being Int_position st b7 in b5 holds
(IExec b2,b6) . b7 = b6 . b7 ) ) ) holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b4) > 0 implies IExec (while>0 b3,b4,b2),b1 = IExec (while>0 b3,b4,b2),(IExec b2,b1) ) )
proof end;

theorem Th29: :: SCMPDS_8:29
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6 being set st card b2 > 0 & ( for b7 being Int_position st b7 in b6 holds
b1 . b7 >= b5 + (b1 . (DataLoc (b1 . b3),b4)) ) & ( for b7 being State of SCMPDS st ( for b8 being Int_position st b8 in b6 holds
b7 . b8 >= b5 + (b7 . (DataLoc (b1 . b3),b4)) ) & b7 . b3 = b1 . b3 & b7 . (DataLoc (b1 . b3),b4) > 0 holds
( (IExec b2,b7) . b3 = b7 . b3 & b2 is_closed_on b7 & b2 is_halting_on b7 & (IExec b2,b7) . (DataLoc (b1 . b3),b4) < b7 . (DataLoc (b1 . b3),b4) & ( for b8 being Int_position st b8 in b6 holds
(IExec b2,b7) . b8 >= b5 + ((IExec b2,b7) . (DataLoc (b1 . b3),b4)) ) ) ) holds
( while>0 b3,b4,b2 is_closed_on b1 & while>0 b3,b4,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b4) > 0 implies IExec (while>0 b3,b4,b2),b1 = IExec (while>0 b3,b4,b2),(IExec b2,b1) ) )
proof end;