let s be State of SCMPDS ; for n being Element of NAT holds (IExec (sum n),s) . (intpos 3) = n
let n be Element of NAT ; (IExec (sum n),s) . (intpos 3) = n
set i1 = GBP := 0 ;
set i2 = GBP ,2 := n;
set i3 = GBP ,3 := 0 ;
set i4 = AddTo GBP ,3,1;
set FD = for-down GBP ,2,1,(Load (AddTo GBP ,3,1));
set a = intpos 3;
set I2 = (GBP := 0 ) ';' (GBP ,2 := n);
set s1 = IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s;
set s2 = Exec (GBP := 0 ),(Initialize s);
set I3 = ((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 );
set s3 = IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s;
A1:
((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 ) is_closed_on s
by SCMPDS_6:34;
A2:
((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 ) is_halting_on s
by SCMPDS_6:35;
A3:
(Exec (GBP := 0 ),(Initialize s)) . GBP = 0
by SCMPDS_2:57;
then A4:
DataLoc ((Exec (GBP := 0 ),(Initialize s)) . GBP ),2 = intpos (0 + 2)
by SCMP_GCD:5;
A5: (IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s) . GBP =
(Exec (GBP ,2 := n),(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 ,2 := n)),s) . GBP ),3 = intpos (0 + 3)
by SCMP_GCD:5;
A7: (IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s) . GBP =
(Exec (GBP ,3 := 0 ),(IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s)) . GBP
by SCMPDS_5:46
.=
0
by A5, A6, AMI_3:52, SCMPDS_2:58
;
then A8:
for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_halting_on IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s
by Th69;
A9: (IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s) . (intpos 2) =
(Exec (GBP ,3 := 0 ),(IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s)) . (intpos 2)
by SCMPDS_5:46
.=
(IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s) . (intpos 2)
by A6, AMI_3:52, SCMPDS_2:58
.=
(Exec (GBP ,2 := n),(Exec (GBP := 0 ),(Initialize s))) . (intpos 2)
by SCMPDS_5:47
.=
n
by A4, SCMPDS_2:58
;
A10: (IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s) . (intpos 3) =
(Exec (GBP ,3 := 0 ),(IExec ((GBP := 0 ) ';' (GBP ,2 := n)),s)) . (intpos 3)
by SCMPDS_5:46
.=
0
by A6, SCMPDS_2:58
;
for-down GBP ,2,1,(Load (AddTo GBP ,3,1)) is_closed_on IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s
by A7, Th69;
hence (IExec (sum n),s) . (intpos 3) =
(IExec (for-down GBP ,2,1,(Load (AddTo GBP ,3,1))),(IExec (((GBP := 0 ) ';' (GBP ,2 := n)) ';' (GBP ,3 := 0 )),s)) . (intpos 3)
by A1, A2, A8, Th49
.=
n
by A10, A7, A9, Th70
;
verum