let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
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)))))),P,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)))))),P,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,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 s,P )
let s be 0 -started 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)))))),P,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)))))),P,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,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 s,P )
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)))))),P,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)))))),P,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,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 s,P ) )
set a = GBP ;

A1: now :: thesis: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
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)))),Q,t)) . GBP = 0 & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,t)) . (intpos 2) = Fib ((k + 1) + 1) )

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS
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)))),Q,t)) . GBP = 0 & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,t)) . (intpos 2) = Fib ((k + 1) + 1) )
let Q be Instruction-Sequence 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)))),Q,t)) . GBP = 0 & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . GBP = 0 & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . GBP = 0 & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . GBP = 0 by A4, Lm4; :: thesis: ( ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_closed_on t,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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,Q & ((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1))) is_halting_on t,Q ) by SCMPDS_6:20, SCMPDS_6:21; :: thesis: ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 3) = (t . (intpos 3)) - 1 by A4, Lm4; :: thesis: ( (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,t)) . (intpos 1) = Fib (k + 1) & (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 1) = Fib (k + 1) by A3, A4, Lm4; :: thesis: (IExec ((((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))),Q,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)))),Q,t)) . (intpos 2) = (t . (intpos 1)) + (t . (intpos 2)) by A4, Lm4
.= 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)))))),P,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)))))),P,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,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 s,P )
hence ( (IExec ((while>0 (GBP,3,(((((GBP,4) := (GBP,2)) ';' (AddTo (GBP,2,GBP,1))) ';' ((GBP,1) := (GBP,4))) ';' (AddTo (GBP,3,(- 1)))))),P,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)))))),P,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,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 s,P ) by A1, Th6; :: thesis: verum