let n, p0 be 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 for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds insert-sort (n,p0) is_halting_on s,Plet s be
State of
SCMPDS;
for P being Instruction-Sequence of SCMPDS holds insert-sort (n,p0) is_halting_on s,Plet P be
Instruction-Sequence of
SCMPDS;
insert-sort (n,p0) is_halting_on s,Pset s1 =
IExec (
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),
P,
(Initialize s));
set s2 =
IExec (
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),
P,
(Initialize s));
set P1 =
P;
set s3 =
IExec (
((GBP := 0) ';' ((GBP,1) := 0)),
P,
(Initialize s));
set s4 =
Exec (
(GBP := 0),
(Initialize s));
A2:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . GBP = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s)))) . GBP
by SCMPDS_5:15;
A3:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 1) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s)))) . (intpos 1)
by SCMPDS_5:15;
A4:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 3) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s)))) . (intpos 3)
by SCMPDS_5:15;
A5:
(
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0) is_closed_on s,
P &
(((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0) is_halting_on s,
P )
by SCMPDS_6:20, SCMPDS_6:21;
A6:
(Exec ((GBP := 0),(Initialize s))) . GBP = 0
by SCMPDS_2:45;
then A7:
DataLoc (
((Exec ((GBP := 0),(Initialize s))) . GBP),1)
= intpos (0 + 1)
by SCMP_GCD:1;
A8:
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,(Initialize s))) . GBP =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP
by SCMPDS_5:42
.=
0
by A6, A7, AMI_3:10, SCMPDS_2:46
;
then A9:
DataLoc (
((IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,(Initialize s))) . GBP),2)
= intpos (0 + 2)
by SCMP_GCD:1;
A10:
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,(Initialize s))) . (intpos 1) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1)
by SCMPDS_5:42
.=
0
by A7, SCMPDS_2:46
;
A11:
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))) . (intpos 1) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,(Initialize s))))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A10, A9, AMI_3:10, SCMPDS_2:46
;
A12:
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))) . GBP =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,(Initialize s))))) . GBP
by SCMPDS_5:41
.=
0
by A8, A9, AMI_3:10, SCMPDS_2:46
;
then A13:
DataLoc (
((IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))) . GBP),3)
= intpos (0 + 3)
by SCMP_GCD:1;
A14:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 3) =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))))) . (intpos 3)
by SCMPDS_5:41
.=
p0
by A13, SCMPDS_2:46
;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 1) =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A11, A13, AMI_3:10, SCMPDS_2:46
;
then A15:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 3) >= ((IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . (intpos 1)) + 7
by A1, A14;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)),P,(Initialize s))) . GBP =
(Exec (((GBP,3) := p0),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,(Initialize s))))) . GBP
by SCMPDS_5:41
.=
0
by A12, A13, AMI_3:10, SCMPDS_2:46
;
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)),P,(Initialize s))),
P &
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)),P,(Initialize s))),
P )
by A15, Lm12, A2, A3, A4;
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)),
P,
(Initialize s)),
P &
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)),
P,
(Initialize s)),
P )
by SCMPDS_6:125, SCMPDS_6:126;
hence
insert-sort (
n,
p0)
is_halting_on s,
P
by A5, SCMPDS_7:24;
verum end;
hence
insert-sort (n,p0) is parahalting
by SCMPDS_6:21; verum