let s be 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),s) . result = Fib n & (IExec (Fib-macro N,result),s) . N = s . N )
let N, result be read-write Int-Location ; ( 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
; 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 )
let n be Element of NAT ; ( n = s . N implies ( (IExec (Fib-macro N,result),s) . result = Fib n & (IExec (Fib-macro N,result),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 ))),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}))),(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 ))),s);
assume A2:
n = s . N
; ( (IExec (Fib-macro N,result),s) . result = Fib n & (IExec (Fib-macro N,result),s) . N = s . N )
A3:
not 1 -stRWNotIn {N,result} in {N,result}
by SFMASTR1:21;
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:21;
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:21;
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 ))),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)),s)) . N
by SCMFSA6C:7
.=
(IExec (((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)),s) . N
by A4, SCMFSA_2:89
.=
(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:9
.=
(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:91
.=
(Initialized s) . N
by A8, SCMFSA_2:89
.=
s . N
by SCMFSA6C:3
;
then A10:
DataPart (IExec (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))),(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 ))),s)) = DataPart ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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 ))),s) . N implies ( ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . $1) . result = Fib $1 & ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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:33
.=
{result,(1 -stRWNotIn {N,result})} \/ (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))
by SF_MASTR:18
;
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:21;
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:21;
A16:
1 -stRWNotIn {N,result} <> result
by A3, TARSKI:def 2;
A17:
now let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )assume A18:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
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 ))),s) . N
;
( ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . (k + 1)) . result = Fib (k + 1) & ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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 ))),s) . N
by A19, XXREAL_0:2;
then A21:
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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}))),((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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}))),(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 ))),s)) . (k + 1)) . result =
(IExec ((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}))),(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 ))),s)) . k)) . result
by A14, Th7
.=
(IExec (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}))),(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 ))),s)) . k)))) . result
by SCMFSA8B:12
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:11
.=
(Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k)) . (1 -stRWNotIn {N,result})
by A16, SCMFSA_2:90
.=
Fib (k + 1)
by A18, A20, A19, SCMFSA6C:3, XXREAL_0:2
;
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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}))),(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 ))),s)) . (k + 1)) . (1 -stRWNotIn {N,result}) =
(IExec ((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}))),(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 ))),s)) . k)) . (1 -stRWNotIn {N,result})
by A12, A21, Th7
.=
(IExec (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}))),(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 ))),s)) . k)))) . (1 -stRWNotIn {N,result})
by SCMFSA8B:12
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k))) . result
by SCMFSA6C:11
.=
((Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k)) . result) + ((Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k)) . (1 -stRWNotIn {N,result}))
by SCMFSA_2:90
.=
(((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k) . result) + ((Initialized ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k)) . (1 -stRWNotIn {N,result}))
by SCMFSA6C:3
.=
(((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k) . result) + (((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . k) . (1 -stRWNotIn {N,result}))
by SCMFSA6C:3
.=
Fib ((k + 1) + 1)
by A18, A20, A19, PRE_FF:1, XXREAL_0:2
;
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 ))),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)),s)) . (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))
by SCMFSA6C:7
.=
(IExec (((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)),s) . (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))
by A13, SCMFSA_2:89
.=
(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:9
.=
(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:91
.=
(Initialized s) . N
by SCMFSA_2:89
.=
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 & (((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 )
by SCMFSA7B:24, SCMFSA7B:25;
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 ))),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)),s)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:7
.=
(IExec (((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)),s) . (intloc 0 )
by SCMFSA_2:89
.=
(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:9
.=
(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:91
.=
(Initialized s) . (intloc 0 )
by SCMFSA_2:89
.=
Fib (0 + 1)
by PRE_FF:1, SCMFSA6C:3
;
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 ))),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)),s)) . (intloc 0 )
by SCMFSA6C:7
.=
(IExec (((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)),s) . (intloc 0 )
by SCMFSA_2:89
.=
(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:9
.=
(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:91
.=
(Initialized s) . (intloc 0 )
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
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 ))),s
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 ))),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)),s)) . result
by SCMFSA6C:7
.=
(IExec (((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)),s) . result
by A16, SCMFSA_2:89
.=
(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:9
.=
((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:91
.=
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 ))),s) . N
;
( ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . 0 ) . result = Fib 0 & ((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . 0 ) . (1 -stRWNotIn {N,result}) = Fib (0 + 1) )
A29:
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),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 ))),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}))),(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 ))),s)) . 0 ) . result = Fib 0
by A14, A27, Th7;
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . 0 ) . (1 -stRWNotIn {N,result}) = Fib (0 + 1)
thus
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . 0 ) . (1 -stRWNotIn {N,result}) = Fib (0 + 1)
by A12, A24, A29, Th7;
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 ))),s
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 ))),s) & 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 ))),s) )
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
by A26, A23, SFMASTR1:3;
hence (IExec (Fib-macro N,result),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}))))),s)) . result
by A26, A31, A23, SFMASTR1:4, SFMASTR1:12
.=
(IExec (i02 ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))),s) . result
by A1, SCMFSA_2:89
.=
(IExec (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))),(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 ))),s)) . result
by A26, A31, SFMASTR1:8
.=
((StepTimes N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))),(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 ))),s)) . n) . result
by A10, SCMFSA6A:38
.=
Fib n
by A9, A30, A2
;
(IExec (Fib-macro N,result),s) . N = s . N
thus (IExec (Fib-macro N,result),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}))))),s)) . N
by A26, A31, A23, A33, SFMASTR1:4, SFMASTR1:12
.=
(IExec (i02 ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))),s) . (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))
by SCMFSA_2:89
.=
(IExec (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))),(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 ))),s)) . (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))
by A26, A31, SFMASTR1:8
.=
s . N
by A7, A22, A32, Th3
; verum