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),s) . result = Fib n & (IExec (Fib_macro N,result),s) . N = s . N )
set D = Int-Locations \/ FinSeq-Locations ;
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),s) . result = Fib n & (IExec (Fib_macro N,result),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),s) . result = Fib n & (IExec (Fib_macro N,result),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})))))),s;
reconsider I301 = (AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})) as parahalting good 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),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),s1) . result = Fib (m + $1) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),s) . result = Fib n & (IExec (Fib_macro N,result),s) . N = s . N ) )
assume A2: n = s . N ; :: thesis: ( (IExec (Fib_macro N,result),s) . result = Fib n & (IExec (Fib_macro N,result),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})))))),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 ))),s)) . (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:7
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA_2:89
.= (Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:7
.= (IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A5, SCMFSA_2:89
.= (Exec (SubFrom result,result),(Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s))) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:9
.= (Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A6, SCMFSA_2:91
.= (Initialize s) . N by SCMFSA_2:89
.= s . N by SCMFSA6C:3 ;
A8: swap result,(1 -stRWNotIn {N,result}) does_not_destroy 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 Initialize s by SCMFSA7B:24;
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})))))),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 ))),s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:7
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A4, SCMFSA_2:89
.= (Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:7
.= (IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A5, SCMFSA_2:89
.= (Exec (SubFrom result,result),(Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s))) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:9
.= (Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A6, SCMFSA_2:91
.= (Initialize s) . N by SCMFSA_2:89
.= 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 Initialize s by SCMFSA7B:25;
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 Macro (AddTo result,(1 -stRWNotIn {N,result})) does_not_destroy 1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result}))) by A12, SCMFSA7B:13, SCMFSA8C:77;
then A14: I301 does_not_destroy 1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result}))) by A8, SCMFSA8C:81;
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),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),s1) . result = Fib (m + (n + 1)) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),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),s1) . result = Fib (m + (n + 1)) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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 ))),s1;
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 ))),s1) . (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) = (n + 1) - 1 by A14, A18, SCMFSA8C:124
.= n ;
A21: (IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),s1) . (intloc 0 ) = (Exec (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 )),(IExec I301,s1)) . (intloc 0 ) by SCMFSA6C:7
.= (IExec I301,s1) . (intloc 0 ) by SCMFSA_2:91
.= 1 by SCMFSA6B:35 ;
A22: DataPart (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) = DataPart (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),s1)) by A14, A19, SCMFSA8C:124;
hence (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) = (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),s1)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6A:38
.= (IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),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,s1)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6C:7
.= (IExec I301,s1) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A4, SCMFSA_2:91
.= (IExec (swap result,(1 -stRWNotIn {N,result})),(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1))) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA8B:12
.= (Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by Th21, SCMFSA6B:22
.= (Initialize s1) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A6, SCMFSA_2:90
.= 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),s1) . result = Fib (m + (n + 1)) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),s1) . result = Fib (m + (n + 1)) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),s1) . result = Fib (m + (n + 1)) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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 ))),s1) . (1 -stRWNotIn {N,result}) = (Exec (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 )),(IExec I301,s1)) . (1 -stRWNotIn {N,result}) by SCMFSA6C:7
.= (IExec I301,s1) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:91
.= (IExec (swap result,(1 -stRWNotIn {N,result})),(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1))) . (1 -stRWNotIn {N,result}) by SCMFSA8B:12
.= (Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1)) . result by SCMFSA6C:11
.= ((Initialize s1) . result) + ((Initialize s1) . (1 -stRWNotIn {N,result})) by SCMFSA_2:90
.= (s1 . result) + ((Initialize 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 ))),s1) . result = (Exec (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 )),(IExec I301,s1)) . result by SCMFSA6C:7
.= (IExec I301,s1) . result by A12, A13, SCMFSA_2:91
.= (IExec (swap result,(1 -stRWNotIn {N,result})),(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1))) . result by SCMFSA8B:12
.= (Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize s1)) . (1 -stRWNotIn {N,result}) by SCMFSA6C:11
.= (Initialize s1) . (1 -stRWNotIn {N,result}) by A3, SCMFSA_2:90
.= Fib (m + 1) by A24, SCMFSA6C:3 ;
thus (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . result = (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),s1)) . result by A22, SCMFSA6A:38
.= 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),s1) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + (n + 1))
thus (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (1 -stRWNotIn {N,result}) = (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(IExec (I301 ';' (SubFrom (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),(intloc 0 ))),s1)) . (1 -stRWNotIn {N,result}) by A22, SCMFSA6A:38
.= 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})))))),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 ))),s)) . result by SCMFSA6C:7
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . result by A12, A13, SCMFSA_2:89
.= (Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s)) . result by SCMFSA6C:7
.= (IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s) . result by A3, SCMFSA_2:89
.= (Exec (SubFrom result,result),(Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s))) . result by SCMFSA6C:9
.= ((Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . result) - ((Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . result) by SCMFSA_2:91
.= 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})))))),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 ))),s)) . (1 -stRWNotIn {N,result}) by SCMFSA6C:7
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . (1 -stRWNotIn {N,result}) by A12, A15, SCMFSA_2:89
.= (Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s)) . (1 -stRWNotIn {N,result}) by SCMFSA6C:7
.= (IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s) . (intloc 0 ) by SCMFSA_2:89
.= (Exec (SubFrom result,result),(Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s))) . (intloc 0 ) by SCMFSA6C:9
.= (Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . (intloc 0 ) by SCMFSA_2:91
.= (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= Fib (0 + 1) by PRE_FF:1, SCMFSA6C:3 ;
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})))))),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 ))),s)) . (intloc 0 ) by SCMFSA6C:7
.= (IExec ((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . (intloc 0 ) by SCMFSA_2:89
.= (Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s)) . (intloc 0 ) by SCMFSA6C:7
.= (IExec (((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)),s) . (intloc 0 ) by SCMFSA_2:89
.= (Exec (SubFrom result,result),(Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s))) . (intloc 0 ) by SCMFSA6C:9
.= (Exec ((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N),(Initialize s)) . (intloc 0 ) by SCMFSA_2:91
.= (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
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})))))),s by A14, SCMFSA8C:119;
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),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),s1) . result = Fib (m + 0 ) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),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),s1) . result = Fib (m + 0 ) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0 ) ) ) )
A34: DataPart (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) = DataPart s1 by A32, A33, SCMFSA8C:123;
hence (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) = s1 . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA6A:38; :: 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),s1) . result = Fib (m + 0 ) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),s1) . result = Fib (m + 0 ) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),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),s1) . result = Fib (m + 0 ) & (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0 ) )
thus (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . result = Fib (m + 0 ) by A34, A35, SCMFSA6A:38; :: thesis: (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0 )
thus (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),s1) . (1 -stRWNotIn {N,result}) = Fib ((m + 1) + 0 ) by A34, A36, SCMFSA6A:38; :: 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})))))),s by A14, A29, SCMFSA8C:119;
A39: i02 ';' (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301) is_closed_on Initialize s by A11, A30, A9, Th3;
hence (IExec (Fib_macro N,result),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)),s)) . result by A11, A30, A38, A9, Th4, Th12
.= (IExec (i02 ';' (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301)),s) . result by A1, SCMFSA_2:89
.= (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(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})))))),s)) . result by A30, A38, Th8
.= Fib (0 + n) by A37, A29, A27, A28, A7, A2
.= Fib n ;
:: thesis: (IExec (Fib_macro N,result),s) . N = s . N
thus (IExec (Fib_macro N,result),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)),s)) . N by A11, A30, A38, A9, A39, Th4, Th12
.= (IExec (i02 ';' (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301)),s) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by SCMFSA_2:89
.= (IExec (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),I301),(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})))))),s)) . (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) by A30, A38, Th8
.= s . N by A37, A29, A10, A7, A2 ; :: thesis: verum