let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence 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 p be Instruction-Sequence 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 )
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 ) )
set i1 = SubFrom (result,result);
set next = 1 -stRWNotIn {N,result};
set Nsave = 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))));
set i0 = (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N;
set i2 = (1 -stRWNotIn {N,result}) := (intloc 0);
set i30 = AddTo (result,(1 -stRWNotIn {N,result}));
set I31 = swap (result,(1 -stRWNotIn {N,result}));
set I301 = (AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})));
set i02 = (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0));
set s1 = IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s);
set I3 = times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))));
set ST = StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)));
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 )
A3: not 1 -stRWNotIn {N,result} in {N,result} by SFMASTR1:20;
then A4: 1 -stRWNotIn {N,result} <> N by TARSKI:def 2;
A5: {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) c= UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) by Th8;
A6: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) = 1 -stRWNotIn (UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by SFMASTR1:def 4;
then A7: not 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) in UsedIntLoc (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) by SFMASTR1:20;
N in {N} by TARSKI:def 1;
then N in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def 3;
then A8: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) <> N by A6, A5, SFMASTR1:20;
A9: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)))) . N by SCMFSA6C:6
.= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)) . N by A4, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . N by SCMFSA6C:8
.= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . N by A1, SCMFSA_2:65
.= (Initialized s) . N by A8, SCMFSA_2:63
.= s . N by SCMFSA6C:3 ;
then A10: DataPart (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) = DataPart ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . n) by A2, Th23;
defpred S1[ Nat] means ( $1 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N implies ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . $1) . result = Fib $1 & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . $1) . (1 -stRWNotIn {N,result}) = Fib ($1 + 1) ) );
set UIFS = (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations;
set i4 = N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))));
A11: UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))) = (UsedIntLoc (AddTo (result,(1 -stRWNotIn {N,result})))) \/ (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by SF_MASTR:29
.= {result,(1 -stRWNotIn {N,result})} \/ (UsedIntLoc (swap (result,(1 -stRWNotIn {N,result})))) by SF_MASTR:14 ;
1 -stRWNotIn {N,result} in {result,(1 -stRWNotIn {N,result})} by TARSKI:def 2;
then A12: 1 -stRWNotIn {N,result} in UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))) by A11, XBOOLE_0:def 3;
then 1 -stRWNotIn {N,result} in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def 3;
then A13: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) <> 1 -stRWNotIn {N,result} by A6, A5, SFMASTR1:20;
result in {result,(1 -stRWNotIn {N,result})} by TARSKI:def 2;
then A14: result in UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))) by A11, XBOOLE_0:def 3;
then result in {N} \/ (UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) by XBOOLE_0:def 3;
then A15: 1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) <> result by A6, A5, SFMASTR1:20;
A16: 1 -stRWNotIn {N,result} <> result by A3, TARSKI:def 2;
A17: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A18: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
A19: k < k + 1 by NAT_1:13;
assume A20: k + 1 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N ; :: thesis: ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . result = Fib (k + 1) & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = Fib ((k + 1) + 1) )
then k < (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N by A19, XXREAL_0:2;
then A21: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) by Th21;
hence ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . result = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) . result by A14, Th7
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))))) . result by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:10
.= (Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result}) by A16, SCMFSA_2:64
.= Fib (k + 1) by A18, A20, A19, SCMFSA6C:3, XXREAL_0:2 ;
:: thesis: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = Fib ((k + 1) + 1)
thus ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (k + 1)) . (1 -stRWNotIn {N,result}) = (IExec (((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k))) . (1 -stRWNotIn {N,result}) by A12, A21, Th7
.= (IExec ((swap (result,(1 -stRWNotIn {N,result}))),(p +* (times* (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))))) . (1 -stRWNotIn {N,result}) by SCMFSA8B:9
.= (Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)))) . result by SCMFSA6C:10
.= ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . result) + ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result})) by SCMFSA_2:64
.= (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . result) + ((Initialized ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k)) . (1 -stRWNotIn {N,result})) by SCMFSA6C:3
.= (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . result) + (((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . k) . (1 -stRWNotIn {N,result})) by SCMFSA6C:3
.= Fib ((k + 1) + 1) by A18, A20, A19, PRE_FF:1, XXREAL_0:2 ; :: thesis: verum
end;
end;
A22: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA6C:6
.= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by A13, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA6C:8
.= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by A15, SCMFSA_2:65
.= (Initialized s) . N by SCMFSA_2:63
.= s . N by SCMFSA6C:3 ;
A23: ( (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0)) is_halting_on Initialized s,p & (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0)) is_closed_on Initialized s,p ) by SCMFSA7B:18, SCMFSA7B:19;
reconsider i02 = (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0)) as good Program of SCM+FSA ;
A24: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stRWNotIn {N,result}) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)))) . (1 -stRWNotIn {N,result}) by SCMFSA6C:6
.= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (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 ;
A25: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (intloc 0) = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)))) . (intloc 0) by SCMFSA6C:6
.= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)) . (intloc 0) by SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . (intloc 0) by SCMFSA6C:8
.= (Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (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 A26: times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) is_closed_on IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s),p by Th24;
A27: (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . result = (Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)))) . result by SCMFSA6C:6
.= (IExec ((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))),p,s)) . result by A16, SCMFSA_2:63
.= (Exec ((SubFrom (result,result)),(Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))))) . result by SCMFSA6C:8
.= ((Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . result) - ((Exec (((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N),(Initialized s))) . result) by SCMFSA_2:65
.= Fib 0 by PRE_FF:1 ;
A28: S1[ 0 ]
proof
assume 0 <= (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N ; :: thesis: ( ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . result = Fib 0 & ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) )
A29: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) = (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) | ((UsedIntLoc ((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) \/ FinSeq-Locations) by A25, Th19;
hence ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . result = Fib 0 by A14, A27, Th7; :: thesis: ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1)
thus ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . 0) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) by A12, A24, A29, Th7; :: thesis: verum
end;
A30: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A28, A17);
 A31: times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) is_halting_on IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s),p by A25, Th24;
then A32: ( times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) is_closed_on Initialized (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)),p & times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))) is_halting_on Initialized (IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)),p ) by A25, A26, Th5;
A33: i02 ';' (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))) is_closed_on Initialized s,p by A26, A23, SFMASTR1:2;
hence (IExec ((Fib-macro (N,result)),p,s)) . result = (Exec ((N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))))),(IExec ((i02 ';' (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . result by A26, A31, A23, SFMASTR1:3, SFMASTR1:11
.= (IExec ((i02 ';' (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . result by A1, SCMFSA_2:63
.= (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . result by A26, A31, SFMASTR1:7
.= ((StepTimes (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . n) . result by A10, SCMFSA6A:7
.= Fib n by A9, A30, A2 ;
:: thesis: (IExec ((Fib-macro (N,result)),p,s)) . N = s . N
thus (IExec ((Fib-macro (N,result)),p,s)) . N = (Exec ((N := (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))))),(IExec ((i02 ';' (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)))) . N by A26, A31, A23, A33, SFMASTR1:3, SFMASTR1:11
.= (IExec ((i02 ';' (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))),p,s)) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by SCMFSA_2:63
.= (IExec ((times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result})))))),p,(IExec (((((1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) := N) ';' (SubFrom (result,result))) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stNotUsed (times (N,((AddTo (result,(1 -stRWNotIn {N,result}))) ';' (swap (result,(1 -stRWNotIn {N,result}))))))) by A26, A31, SFMASTR1:7
.= s . N by A7, A22, A32, Th3 ; :: thesis: verum