let s be 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 ),(Initialized s);
A1: (Exec (GBP := 0 ),(Initialized s)) . GBP = 0 by SCMPDS_2:57;
A2: (IExec ((GBP := 0 ) ';' ((intpos 1) := 0 )),s) . GBP = (Exec ((intpos 1) := 0 ),(Exec (GBP := 0 ),(Initialized 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 ),(Initialized 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