let s be State of SCMPDS ; :: thesis: for n being Element of NAT st s . GBP = 0 & s . (intpos 1) = 0 & s . (intpos 2) = 1 & s . (intpos 3) = n holds
( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 1) = Fib n & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 2) = Fib (n + 1) & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_closed_on 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 s )
let n be Element of NAT ; :: thesis: ( s . GBP = 0 & s . (intpos 1) = 0 & s . (intpos 2) = 1 & s . (intpos 3) = n implies ( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 1) = Fib n & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 2) = Fib (n + 1) & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_closed_on 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 s ) )
set a = GBP ;

A1: now

let t be State of SCMPDS ; :: thesis: for k being Element of NAT st n = (t . (intpos 3)) + k & t . (intpos 1) = Fib k & t . (intpos 2) = Fib (k + 1) & t . GBP = 0 & t . (intpos 3) > 0 holds
( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . GBP = 0 & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_closed_on t & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_halting_on t & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) )
let k be Element of NAT ; :: thesis: ( n = (t . (intpos 3)) + k & t . (intpos 1) = Fib k & t . (intpos 2) = Fib (k + 1) & t . GBP = 0 & t . (intpos 3) > 0 implies ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . GBP = 0 & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_closed_on t & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_halting_on t & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) ) )
assume that
n = (t . (intpos 3)) + k and
A2: t . (intpos 1) = Fib k and
A3: t . (intpos 2) = Fib (k + 1) and
A4: t . GBP = 0 and
t . (intpos 3) > 0 ; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . GBP = 0 & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_closed_on t & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_halting_on t & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) )
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . GBP = 0 by A4, Lm5; :: thesis: ( (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_closed_on t & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_halting_on t & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) )
thus ( (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_closed_on t & (((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)) is_halting_on t ) by SCMPDS_6:34, SCMPDS_6:35; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) )
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 3) = (t . (intpos 3)) - 1 by A4, Lm5; :: thesis: ( (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) & (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1) )
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 1) = Fib (k + 1) by A3, A4, Lm5; :: thesis: (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = Fib ((k + 1) + 1)
thus (IExec ((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))),t) . (intpos 2) = (t . (intpos 1)) + (t . (intpos 2)) by A4, Lm5
.= Fib ((k + 1) + 1) by A2, A3, PRE_FF:1 ; :: thesis: verum

end;

assume ( s . GBP = 0 & s . (intpos 1) = 0 & s . (intpos 2) = 1 & s . (intpos 3) = n ) ; :: thesis: ( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 1) = Fib n & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 2) = Fib (n + 1) & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_closed_on 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 s )
hence ( (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 1) = Fib n & (IExec (while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1)))),s) . (intpos 2) = Fib (n + 1) & while>0 GBP ,3,((((GBP ,4 := GBP ,2) ';' (AddTo GBP ,2,GBP ,1)) ';' (GBP ,1 := GBP ,4)) ';' (AddTo GBP ,3,(- 1))) is_closed_on 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 s ) by A1, Lm6, Th10; :: thesis: verum