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

definition
let f be FinSequence of INT ;
let s be State of SCMPDS ;
let m be Nat;
pred f is_FinSequence_on s,m means :Def1: :: SCPISORT:def 1
for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i));
end;

:: deftheorem Def1 defines is_FinSequence_on SCPISORT:def 1 :
for f being FinSequence of INT
for s being State of SCMPDS
for m being Nat holds
( f is_FinSequence_on s,m iff for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) );

Lm1: for f being FinSequence of INT
for k being Nat holds f is_non_decreasing_on k,k
proof end;

theorem Th1: :: SCPISORT:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of INT
for m, n being Nat st m >= n holds
f is_non_decreasing_on m,n
proof end;

theorem Th2: :: SCPISORT:2  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 n, m being Nat ex f being FinSequence of INT st
( len f = n & ( for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )
proof end;

theorem :: SCPISORT:3  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 n, m being Nat ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )
proof end;

theorem Th4: :: SCPISORT:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of INT
for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent
proof end;

set A = the Instruction-Locations of SCMPDS ;

set D = SCM-Data-Loc ;

theorem Th5: :: SCPISORT:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCMPDS st ( for a being Int_position holds s1 . a = s2 . a ) holds
Dstate s1 = Dstate s2
proof end;

theorem Th6: :: SCPISORT:6  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 No-StopCode Program-block
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s & I is_halting_on s holds
( I ';' j is_closed_on s & I ';' j is_halting_on s )
proof end;

theorem :: SCPISORT:7  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 No-StopCode Program-block
for J being parahalting shiftable Program-block
for a being Int_position st I is_closed_on s & I is_halting_on s holds
(IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a
proof end;

theorem :: SCPISORT:8  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 parahalting No-StopCode Program-block
for J being shiftable Program-block
for a being Int_position st J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
(IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a
proof end;

theorem :: SCPISORT: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 J being parahalting shiftable Program-block st I is_closed_on s & I is_halting_on s holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
proof end;

theorem :: SCPISORT: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 parahalting Program-block
for J being shiftable Program-block st J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
( I ';' J is_closed_on s & I ';' J is_halting_on s )
proof end;

theorem :: SCPISORT: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 j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s & I is_halting_on s holds
( I ';' j is_closed_on s & I ';' j is_halting_on s )
proof end;

Lm2: for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds card (stop (for-down a,i,n,I)) = (card I) + 4
proof end;

Lm3: for a being Int_position
for i being Integer
for n being Nat
for I being Program-block holds for-down a,i,n,I = (a,i <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo a,i,(- n))) ';' (goto (- ((card I) + 2))))
proof end;

Lm4: for I being Program-block
for a being Int_position
for i being Integer
for n being Nat holds Shift (I ';' (AddTo a,i,(- n))),1 c= for-down a,i,n,I
proof end;

scheme :: SCPISORT:sch 1
ForDownHalt{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on F1() & for-down F3(),F4(),F5(),F2() is_halting_on F1() )
provided
A1: F5() > 0 and
A2: P1[ Dstate F1()] and
A3: for t being State of SCMPDS st P1[ Dstate t] & t . F3() = F1() . F3() & t . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
proof end;

scheme :: SCPISORT:sch 2
ForDownExec{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & IExec (for-down F3(),F4(),F5(),F2()),F1() = IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) )
provided
A1: F5() > 0 and
A2: F1() . (DataLoc (F1() . F3()),F4()) > 0 and
A3: P1[ Dstate F1()] and
A4: for t being State of SCMPDS st P1[ Dstate t] & t . F3() = F1() . F3() & t . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
proof end;

scheme :: SCPISORT:sch 3
ForDownEnd{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & (IExec (for-down F3(),F4(),F5(),F2()),F1()) . (DataLoc (F1() . F3()),F4()) <= 0 & P1[ Dstate (IExec (for-down F3(),F4(),F5(),F2()),F1())] )
provided
A1: F5() > 0 and
A2: P1[ Dstate F1()] and
A3: for t being State of SCMPDS st P1[ Dstate t] & t . F3() = F1() . F3() & t . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . F3() = t . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t) . (DataLoc (F1() . F3()),F4()) = (t . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on t & F2() is_halting_on t & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),t)] )
proof end;

theorem Th12: :: SCPISORT: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 shiftable No-StopCode Program-block
for a, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
proof end;

theorem Th13: :: SCPISORT: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, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec (I ';' (AddTo a,i,(- n))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)
proof end;

theorem :: SCPISORT: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 n being Nat st s . (DataLoc (s . a),i) > 0 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a 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 ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )
proof end;

definition
let n, p0 be Nat;
func insert-sort n,p0 -> Program-block equals :: SCPISORT:def 2
((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))));
coherence
((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))) is Program-block
;
end;

:: deftheorem defines insert-sort SCPISORT:def 2 :
for n, p0 being Nat holds insert-sort n,p0 = ((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (n - 1))) ';' (GBP ,3 := p0)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))));

set j1 = AddTo GBP ,3,1;

set j2 = GBP ,4 := GBP ,3;

set j3 = AddTo GBP ,1,1;

set j4 = GBP ,6 := GBP ,1;

set k1 = GBP ,5 := (intpos 4),(- 1);

set k2 = SubFrom GBP ,5,(intpos 4),0;

set k3 = GBP ,5 := (intpos 4),(- 1);

set k4 = (intpos 4),(- 1) := (intpos 4),0;

set k5 = (intpos 4),0 := GBP ,5;

set k6 = AddTo GBP ,4,(- 1);

set k7 = AddTo GBP ,6,(- 1);

set FA = Load (GBP ,6 := 0);

set TR = ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1));

set IF = if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0));

set B1 = ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)));

set WH = while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))));

set J4 = (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1);

set B2 = ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))));

set FR = for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))));

Lm5: card (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) = 10
proof end;

Lm6: card (((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) = 16
proof end;

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

set a4 = intpos 4;

set a5 = intpos 5;

set a6 = intpos 6;

Lm7: for s being State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . GBP = 0 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 1) = s . (intpos 1) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 2) = s . (intpos 2) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 3) = s . (intpos 3) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 6) < s . (intpos 6) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 4) >= 7 + ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc (s . (intpos 4)),(- 1)) > s . (DataLoc (s . (intpos 4)),0) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),0) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (DataLoc (s . (intpos 4)),0) = s . (DataLoc (s . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc (s . (intpos 4)),(- 1)) <= s . (DataLoc (s . (intpos 4)),0) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (DataLoc (s . (intpos 4)),0) = s . (DataLoc (s . (intpos 4)),0) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s) . (intpos 6) = 0 ) ) )
proof end;

Lm8: for s being State of SCMPDS st s . (intpos 4) >= 7 + (s . (DataLoc (s . GBP ),6)) & s . GBP = 0 holds
( while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) is_closed_on s & while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) is_halting_on s )
proof end;

Lm9: for s being State of SCMPDS st s . (intpos 4) >= 7 + (s . (DataLoc (s . GBP ),6)) & s . GBP = 0 holds
( (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s) . GBP = 0 & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s) . (intpos 1) = s . (intpos 1) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s) . (intpos 2) = s . (intpos 2) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s) . (intpos 3) = s . (intpos 3) )
proof end;

Lm10: for s being State of SCMPDS st s . GBP = 0 holds
( (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . GBP = 0 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos i) = s . (intpos i) ) )
proof end;

set jf = AddTo GBP ,2,(- 1);

set B3 = (((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1));

Lm11: for s being State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 holds
( (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s) . GBP = 0 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 2) = (s . (intpos 2)) - 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos 1) = (s . (intpos 1)) + 1 & ( for i being Nat st i <> 2 holds
(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s) . (intpos i) = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s)) . (intpos i) ) )
proof end;

Lm12: for s being State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 holds
( for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) is_closed_on s & for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) is_halting_on s )
proof end;

Lm13: for s being State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 & s . (intpos 2) > 0 holds
IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),s = IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),s)
proof end;

theorem :: SCPISORT:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, p0 being Nat holds card (insert-sort n,p0) = 23
proof end;

theorem :: SCPISORT:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p0, n being Nat st p0 >= 7 holds
insert-sort n,p0 is parahalting
proof end;

Lm14: for s being State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s = IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),s)
proof end;

set Insertthek1item = while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))));

theorem Th17: :: SCPISORT:17  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 f, g being FinSequence of INT
for k0, k being Nat st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),s,k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being Nat st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
proof end;

Lm15: for s being State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),s,p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
proof end;

theorem :: SCPISORT:18  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 f, g being FinSequence of INT
for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec (insert-sort n,(p0 + 1)),s,p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
proof end;