let s be 0 -started State of SCMPDS; :: thesis: for n being Element of NAT holds
( (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s )
let n be Element of NAT ; :: thesis: ( (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n & (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s )
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)),s);
set t2 = IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s);
set t3 = IExec (((GBP := 0) ';' ((intpos 1) := 0)),s);
set t4 = Exec ((GBP := 0),(Initialize s));
A1: (Exec ((GBP := 0),(Initialize s))) . GBP = 0 by SCMPDS_2:57;
A2: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)) . GBP = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . GBP by SCMPDS_5:47
.= 0 by A1, AMI_3:52, SCMPDS_2:57 ;
A3: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)) . GBP = (Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)))) . GBP by SCMPDS_5:46
.= 0 by A2, AMI_3:52, SCMPDS_2:57 ;
A4: (IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)) . (intpos 1) = (Exec (((intpos 1) := 0),(Exec ((GBP := 0),(Initialize s))))) . (intpos 1) by SCMPDS_5:47
.= 0 by SCMPDS_2:57 ;
A5: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)) . (intpos 1) = (Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)))) . (intpos 1) by SCMPDS_5:46
.= 0 by A4, AMI_3:52, SCMPDS_2:57 ;
A6: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)) . (intpos 1) = (Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)))) . (intpos 1) by SCMPDS_5:46
.= 0 by A5, AMI_3:52, SCMPDS_2:57 ;
A7: (IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)) . (intpos 2) = (Exec (((intpos 2) := 1),(IExec (((GBP := 0) ';' ((intpos 1) := 0)),s)))) . (intpos 2) by SCMPDS_5:46
.= 1 by SCMPDS_2:57 ;
A8: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)) . (intpos 2) = (Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)))) . (intpos 2) by SCMPDS_5:46
.= 1 by A7, AMI_3:52, SCMPDS_2:57 ;
A9: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)) . (intpos 3) = (Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)))) . (intpos 3) by SCMPDS_5:46
.= n by SCMPDS_2:57 ;
A10: (IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)) . GBP = (Exec (((intpos 3) := n),(IExec ((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)),s)))) . GBP by SCMPDS_5:46
.= 0 by A3, AMI_3:52, SCMPDS_2:57 ;
then A11: ( 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)),s) & 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)),s) ) by A6, A8, A9, Lm7;
(IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),(IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)))) . (intpos 1) = Fib n by A10, A6, A8, A9, Lm7;
hence (IExec ((Fib-macro n),s)) . (intpos 1) = Fib n by A11, SCPISORT:8; :: thesis: ( (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) & Fib-macro n is_halting_on s )
(IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),(IExec (((((GBP := 0) ';' ((intpos 1) := 0)) ';' ((intpos 2) := 1)) ';' ((intpos 3) := n)),s)))) . (intpos 2) = Fib (n + 1) by A10, A6, A8, A9, Lm7;
hence (IExec ((Fib-macro n),s)) . (intpos 2) = Fib (n + 1) by A11, SCPISORT:8; :: thesis: Fib-macro n is_halting_on s
thus Fib-macro n is_halting_on s by A11, SCPISORT:10; :: thesis: verum