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