let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for n being Element of NAT holds
( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P )
let s be 0 -started State of SCMPDS; for n being Element of NAT holds
( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P )
let n be Element of NAT ; ( (IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P )
set a = GBP ;
set i1 = GBP := 0;
set i2 = (intpos 1) := 0;
set i3 = (intpos 2) := 1;
set i4 = (intpos 3) := n;
set I4 = (((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n);
set t1 = IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s);
set t2 = IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s);
set t3 = IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s);
set t4 = Exec ((GBP := 0),s);
A1:
Initialize s = s
by MEMSTR_0:44;
A2:
(Exec ((GBP := 0),s)) . GBP = 0
by SCMPDS_2:45;
A3: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)) . GBP =
(Exec (((intpos 1) := 0),(Exec ((GBP := 0),s)))) . GBP
by SCMPDS_5:42
.=
0
by A2, AMI_3:10, SCMPDS_2:45
;
A4: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)) . GBP =
(Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A3, AMI_3:10, SCMPDS_2:45
;
A5: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)) . (intpos 1) =
(Exec (((intpos 1) := 0),(Exec ((GBP := 0),s)))) . (intpos 1)
by SCMPDS_5:42
.=
0
by SCMPDS_2:45
;
A6: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)) . (intpos 1) =
(Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A5, AMI_3:10, SCMPDS_2:45
;
A7: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 1) =
(Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A6, AMI_3:10, SCMPDS_2:45
;
A8: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)) . (intpos 2) =
(Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
1
by SCMPDS_2:45
;
A9: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 2) =
(Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
1
by A8, AMI_3:10, SCMPDS_2:45
;
A10: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 3) =
(Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)))) . (intpos 3)
by SCMPDS_5:41
.=
n
by SCMPDS_2:45
;
A11: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . GBP =
(Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A4, AMI_3:10, SCMPDS_2:45
;
A12:
(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))) . GBP = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . GBP
by SCMPDS_5:15;
A13:
(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))) . (intpos 1) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 1)
by SCMPDS_5:15;
A14:
(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))) . (intpos 2) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 2)
by SCMPDS_5:15;
A15:
(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))) . (intpos 3) = (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)) . (intpos 3)
by SCMPDS_5:15;
A16:
( while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_closed_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)),P & while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_halting_on Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)),P )
by A7, A9, A10, Lm5, A11, A12, A13, A14, A15;
A17:
while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_closed_on IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s),P
proof
for
k being
Nat holds
IC (Comput ((P +* (stop (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))))),(Initialize (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)))),k)) in dom (stop (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))))
by A16, SCMPDS_6:def 2;
hence
while>0 (
GBP,3,
(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))
is_closed_on IExec (
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),
P,
s),
P
by SCMPDS_6:def 2;
verum
end;
A18:
while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))) is_halting_on IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s),P
proof
P +* (stop (while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))))))) halts_on Initialize (Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s)))
by A16, SCMPDS_6:def 3;
hence
while>0 (
GBP,3,
(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))
is_halting_on IExec (
((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),
P,
s),
P
by SCMPDS_6:def 3;
verum
end;
(IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),P,(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))))) . (intpos 1) = Fib n
by A11, A7, A9, A10, Lm5, A12, A13, A14, A15;
hence
(IExec ((Fib-macro n),P,s)) . (intpos 1) = Fib n
by A17, A18, SCPISORT:7; ( (IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s,P )
(IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),P,(Initialize (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),P,s))))) . (intpos 2) = Fib (n + 1)
by A11, A7, A9, A10, Lm5, A12, A13, A14, A15;
hence
(IExec ((Fib-macro n),P,s)) . (intpos 2) = Fib (n + 1)
by A17, A18, SCPISORT:7; Fib-macro n is_halting_on s,P
thus
Fib-macro n is_halting_on s,P
by A17, A18, A1, SCPISORT:9; verum