let p0, n be Element of NAT ; :: thesis: ( p0 >= 7 implies insert-sort n,p0 is parahalting )
assume A1:
p0 >= 7
; :: thesis: 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);
now let s be
State of
SCMPDS ;
:: thesis: 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 ),
(Initialized s);
A2:
(Exec (GBP := 0 ),(Initialized s)) . GBP = 0
by SCMPDS_2:57;
then A3:
DataLoc ((Exec (GBP := 0 ),(Initialized 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 ),(Initialized s))) . GBP
by SCMPDS_5:47
.=
0
by A2, A3, AMI_3:52, SCMPDS_2:58
;
A6:
(IExec ((GBP := 0 ) ';' (GBP ,1 := 0 )),s) . (intpos 1) =
(Exec (GBP ,1 := 0 ),(Exec (GBP := 0 ),(Initialized s))) . (intpos 1)
by SCMPDS_5:47
.=
0
by A3, SCMPDS_2:58
;
A7:
DataLoc ((IExec ((GBP := 0 ) ';' (GBP ,1 := 0 )),s) . GBP ),2
= intpos (0 + 2)
by A5, SCMP_GCD:5;
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, A7, AMI_3:52, SCMPDS_2:58
;
A11:
(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 A6, A7, AMI_3:52, SCMPDS_2:58
;
A12:
DataLoc ((IExec (((GBP := 0 ) ';' (GBP ,1 := 0 )) ';' (GBP ,2 := (n - 1))),s) . GBP ),3
= intpos (0 + 3)
by A9, SCMP_GCD:5;
A14:
(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, A12, AMI_3:52, SCMPDS_2:58
;
A16:
(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 A11, A12, AMI_3:52, SCMPDS_2:58
;
A17:
(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 A12, SCMPDS_2:58
;
A18:
(
(((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;
(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, A16, A17;
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 A14, Lm12;
hence
insert-sort n,
p0 is_halting_on s
by A18, SCMPDS_7:43;
:: thesis: verum end;
hence
insert-sort n,p0 is parahalting
by SCMPDS_6:35; :: thesis: verum