let p0, n be Element of NAT ; ( p0 >= 7 implies insert-sort (n,p0) is parahalting )
set a = GBP ;
set i1 = GBP := 0;
set i2 = (GBP,1) := 0;
set i3 = (GBP,2) := (n - 1);
set i4 = (GBP,3) := p0;
set I = (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0);
assume A1:
p0 >= 7
; insert-sort (n,p0) is parahalting
now let s be
State of
SCMPDS;
insert-sort (n,p0) is_halting_on sset s1 =
IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
s);
set s2 =
IExec (
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),
s);
set s3 =
IExec (
((GBP := 0) ';' ((GBP,1) := 0)),
s);
set s4 =
Exec (
(GBP := 0),
(Initialize s));
X1:
IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
s)
= IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
(Initialize s))
by SCMPDS_5:48;
X2:
IExec (
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),
s)
= IExec (
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),
(Initialize s))
by SCMPDS_5:48;
X3:
IExec (
((GBP := 0) ';' ((GBP,1) := 0)),
s)
= IExec (
((GBP := 0) ';' ((GBP,1) := 0)),
(Initialize s))
by SCMPDS_5:48;
X4:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . GBP = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s))) . GBP
by SCMPDS_5:40;
X5:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 1) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s))) . (intpos 1)
by SCMPDS_5:40;
X6:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 3) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s))) . (intpos 3)
by SCMPDS_5:40;
X9:
Initialize (Initialize s) = Initialize s
;
A2:
(
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0) is_closed_on s &
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0) is_halting_on s )
by SCMPDS_6:34, SCMPDS_6:35;
A3:
(Exec ((GBP := 0),(Initialize s))) . GBP = 0
by SCMPDS_2:57;
then A4:
DataLoc (
((Exec ((GBP := 0),(Initialize s))) . GBP),1)
= intpos (0 + 1)
by SCMP_GCD:5;
A5:
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . GBP =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP
by X3, X9, SCMPDS_5:47
.=
0
by A3, A4, AMI_3:52, SCMPDS_2:58
;
then A6:
DataLoc (
((IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . GBP),2)
= intpos (0 + 2)
by SCMP_GCD:5;
A7:
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)) . (intpos 1) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1)
by X3, X9, SCMPDS_5:47
.=
0
by A4, SCMPDS_2:58
;
A8:
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . (intpos 1) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . (intpos 1)
by X2, X3, SCMPDS_5:46
.=
0
by A7, A6, AMI_3:52, SCMPDS_2:58
;
A9:
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . GBP =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),s)))) . GBP
by X2, X3, SCMPDS_5:46
.=
0
by A5, A6, AMI_3:52, SCMPDS_2:58
;
then A10:
DataLoc (
((IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)) . GBP),3)
= intpos (0 + 3)
by SCMP_GCD:5;
A11:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 3) =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos 3)
by X1, X2, SCMPDS_5:46
.=
p0
by A10, SCMPDS_2:58
;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 1) =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . (intpos 1)
by X1, X2, SCMPDS_5:46
.=
0
by A8, A10, AMI_3:52, SCMPDS_2:58
;
then A12:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 3) >= ((IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . (intpos 1)) + 7
by A1, A11;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) . GBP =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),s)))) . GBP
by X1, X2, SCMPDS_5:46
.=
0
by A9, A10, AMI_3:52, SCMPDS_2:58
;
then
(
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 Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),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 Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),s)) )
by A12, Lm13, X4, X5, X6;
then
(
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 IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
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 IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
s) )
by SCMPDS_6:139, SCMPDS_6:140;
hence
insert-sort (
n,
p0)
is_halting_on s
by A2, SCMPDS_7:43;
verum end;
hence
insert-sort (n,p0) is parahalting
by SCMPDS_6:35; verum