:: SCMPDS_8 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

set A = the Instruction-Locations of SCMPDS ;

set D = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position ex i being 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 the Instruction-Locations of SCMPDS implies it . x = goto 0 ) & ( x = IC SCMPDS implies it . x = inspos 0 ) );
existence
ex b1 being State of SCMPDS st
for x being set holds
( ( x in SCM-Data-Loc implies b1 . x = t . x ) & ( x in the Instruction-Locations of SCMPDS implies b1 . x = goto 0 ) & ( x = IC SCMPDS implies b1 . x = inspos 0 ) )
proof end;
uniqueness
for b1, b2 being State of SCMPDS st ( for x being set holds
( ( x in SCM-Data-Loc implies b1 . x = t . x ) & ( x in the Instruction-Locations of SCMPDS implies b1 . x = goto 0 ) & ( x = IC SCMPDS implies b1 . x = inspos 0 ) ) ) & ( for x being set holds
( ( x in SCM-Data-Loc implies b2 . x = t . x ) & ( x in the Instruction-Locations of SCMPDS implies b2 . x = goto 0 ) & ( x = IC SCMPDS implies b2 . x = inspos 0 ) ) ) holds
b1 = b2
proof end;
end;

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

theorem Th2: :: SCMPDS_8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t1, t2 being State of SCMPDS st t1 | SCM-Data-Loc = t2 | SCM-Data-Loc holds
Dstate t1 = Dstate t2
proof end;

theorem Th3: :: SCMPDS_8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for s being State of SCMPDS holds (Dstate s) . a = s . a
proof end;

theorem Th5: :: SCMPDS_8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let a be Int_position ;
let i be Integer;
let I be Program-block;
func while<0 a,i,I -> Program-block 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-block
;
end;

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

registration
let I be shiftable Program-block;
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 No-StopCode Program-block;
let a be Int_position ;
let i be Integer;
cluster while<0 a,i,I -> No-StopCode ;
correctness
coherence
while<0 a,i,I is No-StopCode
;
;
end;

theorem Th6: :: SCMPDS_8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block 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-block holds card (stop (while<0 a,i,I)) = (card I) + 3
proof end;

theorem Th7: :: SCMPDS_8:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for m being Nat
for I being Program-block holds
( m < (card I) + 2 iff inspos m in dom (while<0 a,i,I) )
proof end;

theorem Th8: :: SCMPDS_8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds
( (while<0 a,i,I) . (inspos 0) = a,i >=0_goto ((card I) + 2) & (while<0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1)) )
proof end;

Lm2: for a being Int_position
for i being Integer
for I being Program-block holds while<0 a,i,I = (a,i >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by SCMPDS_4:51;

theorem Th9: :: SCMPDS_8:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
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 & while<0 a,i,I is_halting_on s )
proof end;

theorem Th10: :: SCMPDS_8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a, c being Int_position
for i being Integer st s . (DataLoc (s . a),i) >= 0 holds
IExec (while<0 a,i,I),s = s +* (Start-At (inspos ((card I) + 2)))
proof end;

theorem :: SCMPDS_8:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a being Int_position
for i being Integer st s . (DataLoc (s . a),i) >= 0 holds
IC (IExec (while<0 a,i,I),s) = inspos ((card I) + 2)
proof end;

theorem :: SCMPDS_8:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a, b being Int_position
for i being Integer st s . (DataLoc (s . a),i) >= 0 holds
(IExec (while<0 a,i,I),s) . b = s . b
proof end;

Lm3: for I being Program-block
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{ 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
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) >= 0 and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) < 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

scheme :: SCMPDS_8:sch 2
WhileLExec{ 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
A1: card F3() > 0 and
A2: F2() . (DataLoc (F2() . F4()),F5()) < 0 and
A3: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) >= 0 and
A4: P1[ Dstate F2()] and
A5: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) < 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

theorem :: SCMPDS_8:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & f . (Dstate (IExec I,t)) < f . (Dstate t) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
proof end;

theorem :: SCMPDS_8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 & 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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
proof end;

theorem Th15: :: SCMPDS_8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS 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,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while<0 a,i,I is_closed_on s & while<0 a,i,I is_halting_on s )
proof end;

theorem :: SCMPDS_8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
proof end;

definition
let a be Int_position ;
let i be Integer;
let I be Program-block;
func while>0 a,i,I -> Program-block 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-block
;
end;

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

registration
let I be shiftable Program-block;
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 No-StopCode Program-block;
let a be Int_position ;
let i be Integer;
cluster while>0 a,i,I -> No-StopCode ;
correctness
coherence
while>0 a,i,I is No-StopCode
;
;
end;

theorem Th17: :: SCMPDS_8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds card (while>0 a,i,I) = (card I) + 2
proof end;

Lm4: for a being Int_position
for i being Integer
for I being Program-block holds card (stop (while>0 a,i,I)) = (card I) + 3
proof end;

theorem Th18: :: SCMPDS_8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for m being Nat
for I being Program-block holds
( m < (card I) + 2 iff inspos m in dom (while>0 a,i,I) )
proof end;

theorem Th19: :: SCMPDS_8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int_position
for i being Integer
for I being Program-block holds
( (while>0 a,i,I) . (inspos 0) = a,i <=0_goto ((card I) + 2) & (while>0 a,i,I) . (inspos ((card I) + 1)) = goto (- ((card I) + 1)) )
proof end;

Lm5: for a being Int_position
for i being Integer
for I being Program-block holds while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by SCMPDS_4:51;

theorem Th20: :: SCMPDS_8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
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 & while>0 a,i,I is_halting_on s )
proof end;

theorem Th21: :: SCMPDS_8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a, c being Int_position
for i being Integer st s . (DataLoc (s . a),i) <= 0 holds
IExec (while>0 a,i,I),s = s +* (Start-At (inspos ((card I) + 2)))
proof end;

theorem :: SCMPDS_8:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a being Int_position
for i being Integer st s . (DataLoc (s . a),i) <= 0 holds
IC (IExec (while>0 a,i,I),s) = inspos ((card I) + 2)
proof end;

theorem :: SCMPDS_8:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being Program-block
for a, b being Int_position
for i being Integer st s . (DataLoc (s . a),i) <= 0 holds
(IExec (while>0 a,i,I),s) . b = s . b
proof end;

Lm6: for I being Program-block
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{ 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
A1: card F3() > 0 and
A2: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) <= 0 and
A3: P1[ Dstate F2()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) > 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

scheme :: SCMPDS_8:sch 4
WhileGExec{ 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
A1: card F3() > 0 and
A2: F2() . (DataLoc (F2() . F4()),F5()) > 0 and
A3: for t being State of SCMPDS st P1[ Dstate t] & F1((Dstate t)) = 0 holds
t . (DataLoc (F2() . F4()),F5()) <= 0 and
A4: P1[ Dstate F2()] and
A5: for t being State of SCMPDS st P1[ Dstate t] & t . F4() = F2() . F4() & t . (DataLoc (F2() . F4()),F5()) > 0 holds
( (IExec F3(),t) . F4() = t . F4() & F3() is_closed_on t & F3() is_halting_on t & F1((Dstate (IExec F3(),t))) < F1((Dstate t)) & P1[ Dstate (IExec F3(),t)] )
proof end;

theorem Th24: :: SCMPDS_8:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s )
proof end;

theorem Th25: :: SCMPDS_8:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s)
proof end;

theorem :: SCMPDS_8:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
proof end;

theorem Th27: :: SCMPDS_8:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
for a being Int_position
for i, c being Integer
for X, Y 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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
(IExec I,t) . x = t . x ) ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
proof end;

theorem :: SCMPDS_8:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
for a being Int_position
for i being Integer
for X being set st card I > 0 & ( for t being State of SCMPDS 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
proof end;

theorem :: SCMPDS_8:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCMPDS
for I being shiftable No-StopCode Program-block
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 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,t) . a = t . a & I is_closed_on t & I is_halting_on t & (IExec I,t) . (DataLoc (s . a),i) < t . (DataLoc (s . a),i) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) ) ) holds
( while>0 a,i,I is_closed_on s & while>0 a,i,I is_halting_on s & ( s . (DataLoc (s . a),i) > 0 implies IExec (while>0 a,i,I),s = IExec (while>0 a,i,I),(IExec I,s) ) )
proof end;