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);
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 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 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 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 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 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 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 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 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 A12, Lm13;
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