let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
let s be State of SCM+FSA; :: thesis: for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
let N, result be read-write Int-Location ; :: thesis: ( N <> result implies for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N ) )
assume A1: N <> result ; :: thesis: for n being Element of NAT st n = s . N holds
( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
set i0 = SubFrom (result,result);
set next = 1 -stRWNotIn {N,result};
set aux = 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))));
set Nsave = 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))));
set i00 = (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N;
set i1 = (1 -stRWNotIn {N,result}) := (intloc 0);
set i2 = (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))));
set i30 = AddTo (result,(1 -stRWNotIn {N,result}));
set I31 = swap (result,(1 -stRWNotIn {N,result}));
set i02 = ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))));
set s1 = IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s);
set p1 = p;
reconsider I301 = (AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))) as good parahalting Program of SCM+FSA ;
set I3 = Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301);
set i4 = N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))));
defpred S1[ Element of NAT ] means for s1 being State of SCM+FSA st $1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + $1) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + $1) ) ) );
let n be Element of NAT ; :: thesis: ( n = s . N implies ( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N ) )
assume A2: n = s . N ; :: thesis: ( (IExec ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )
not 1 -stRWNotIn {N,result} in {N,result} by Th21;
then A3: result <> 1 -stRWNotIn {N,result} by TARSKI:def 2;
A4: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by Th22;
A5: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> 1 -stRWNotIn {N,result} by Th21, Th23;
A6: 2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) <> result by Th21, Th23;
A7: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A5, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:65
.= (Initialized s) . N by SCMFSA_2:63
.= s . N by SCMFSA6C:3 ;
A8: not swap (result,(1 -stRWNotIn {N,result})) destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by Th1, Th21;
A9: ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is_closed_on Initialized s,p by SCMFSA7B:18;
A10: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A4, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A5, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:65
.= (Initialized s) . N by SCMFSA_2:63
.= s . N by SCMFSA6C:3 ;
A11: ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) is_halting_on Initialized s,p by SCMFSA7B:19;
reconsider i02 = ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))) as good Program of SCM+FSA ;
A12: not 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by Th21;
A13: result in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by Th23;
then not Macro (AddTo (result,(1 -stRWNotIn {N,result}))) destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by A12, SCMFSA7B:7, SCMFSA8C:48;
then A14: not I301 destroys 1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by A8, SCMFSA8C:52;
A15: 1 -stRWNotIn {N,result} in UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))) by Th23;
A16: now
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A17: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let s1 be State of SCM+FSA; :: thesis: ( n + 1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) ) ) )
assume that
A18: n + 1 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) and
s1 . (intloc 0) = 1 ; :: thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) ) )
set s2 = IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1);
set p2 = p;
A19: s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) > 0 by A18, NAT_1:3;
then A20: (IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (n + 1) - 1 by A14, A18, SCMFSA8C:91
.= n ;
A21: (IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (intloc 0) = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (intloc 0) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (intloc 0) by SCMFSA_2:65
.= 1 by SCMFSA6B:11 ;
A22: DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) = DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) by A14, A19, SCMFSA8C:91;
hence (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6A:7
.= (IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A17, A20, A21
.= (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A4, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by Th21, SCMFSA6B:3
.= (Initialized s1) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A6, SCMFSA_2:64
.= s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6C:3 ;
:: thesis: for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) )
let m be Element of NAT ; :: thesis: ( s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) ) )
assume that
A23: s1 . result = Fib m and
A24: s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) ; :: thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + (n + 1)) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1)) )
A25: (IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . (1 -stRWNotIn {N,result}) = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec (I301,p,s1)) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . (1 -stRWNotIn {N,result}) by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . result by SCMFSA6C:10
.= ((Initialized s1) . result) + ((Initialized s1) . (1 -stRWNotIn {N,result})) by SCMFSA_2:64
.= (s1 . result) + ((Initialized s1) . (1 -stRWNotIn {N,result})) by SCMFSA6C:3
.= (s1 . result) + (s1 . (1 -stRWNotIn {N,result})) by SCMFSA6C:3
.= Fib ((m + 1) + 1) by A23, A24, PRE_FF:1 ;
A26: (IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)) . result = (Exec ((SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0))),(IExec (I301,p,s1)))) . result by SCMFSA6C:6
.= (IExec (I301,p,s1)) . result by A12, A13, SCMFSA_2:65
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),p,(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))))) . result by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized s1))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:10
.= (Initialized s1) . (1 -stRWNotIn {N,result}) by A3, SCMFSA_2:64
.= Fib (m + 1) by A24, SCMFSA6C:3 ;
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . result by A22, SCMFSA6A:7
.= Fib ((m + 1) + n) by A17, A20, A21, A26, A25
.= Fib (m + (n + 1)) ; :: thesis: (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1))
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((I301 ';' (SubFrom ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),(intloc 0)))),p,s1)))) . (1 -stRWNotIn {N,result}) by A22, SCMFSA6A:7
.= Fib (((m + 1) + 1) + n) by A17, A20, A21, A26, A25
.= Fib ((m + 1) + (n + 1)) ; :: thesis: verum
end;
end;
A27: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . result = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . result by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . result by A12, A13, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)))) . result by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)) . result by A3, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . result by SCMFSA6C:8
.= ((Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . result) - ((Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . result) by SCMFSA_2:65
.= Fib 0 by PRE_FF:1 ;
A28: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stRWNotIn {N,result}) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= Fib (0 + 1) by PRE_FF:1, SCMFSA6A:38 ;
A29: (IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (intloc 0) = (Exec (((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec (((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N),(Initialized s))) . (intloc 0) by SCMFSA_2:65
.= (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA6A:38 ;
then A30: Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301) is_closed_on IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s),p by A14, SCMFSA8C:86;
A31: S1[ 0 ]
proof
let s1 be State of SCM+FSA; :: thesis: ( 0 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & s1 . (intloc 0) = 1 implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) ) ) )
assume that
A32: 0 = s1 . (1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) and
A33: s1 . (intloc 0) = 1 ; :: thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) & ( for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) ) )
A34: DataPart (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) = DataPart s1 by A32, A33, SCMFSA8C:90;
hence (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA6A:7; :: thesis: for m being Element of NAT st s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) holds
( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) )
let m be Element of NAT ; :: thesis: ( s1 . result = Fib m & s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) implies ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) ) )
assume that
A35: s1 . result = Fib m and
A36: s1 . (1 -stRWNotIn {N,result}) = Fib (m + 1) ; :: thesis: ( (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) & (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) )
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . result = Fib (m + 0) by A34, A35, SCMFSA6A:7; :: thesis: (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0)
thus (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,s1)) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0) by A34, A36, SCMFSA6A:7; :: thesis: verum
end;
A37: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A31, A16);
 A38: Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301) is_halting_on IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s),p by A14, A29, SCMFSA8C:86;
A39: i02 ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)) is_closed_on Initialized s,p by A11, A30, A9, Th3;
hence (IExec ((Fib_macro (N,result)),p,s)) . result = (Exec ((N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec ((i02 ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)))) . result by A11, A30, A38, A9, Th4, Th12
.= (IExec ((i02 ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)) . result by A1, SCMFSA_2:63
.= (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . result by A30, A38, Th8
.= Fib (0 + n) by A37, A29, A27, A28, A7, A2
.= Fib n ;
:: thesis: (IExec ((Fib_macro (N,result)),p,s)) . N = s . N
thus (IExec ((Fib_macro (N,result)),p,s)) . N = (Exec ((N := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))))),(IExec ((i02 ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)))) . N by A11, A30, A38, A9, A39, Th4, Th12
.= (IExec ((i02 ';' (Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301))),p,s)) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by SCMFSA_2:63
.= (IExec ((Times ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))),I301)),p,(IExec ((((((2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) := (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . (2 -ndRWNotIn (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result}))))) by A30, A38, Th8
.= s . N by A37, A29, A10, A7, A2 ; :: thesis: verum