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 (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n )
let N, result be read-write Int-Location ; ( N <> result implies for n being Element of NAT st n = s . N holds
( (IExec (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n ) )
assume A1:
N <> result
; for n being Element of NAT st n = s . N holds
( (IExec (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n )
set i0 = SubFrom result,result;
set rem2 = 3 -rdRWNotIn {N,result};
set aux = 2 -ndRWNotIn {N,result};
set next = 1 -stRWNotIn {N,result};
set I3i0 = (3 -rdRWNotIn {N,result}) := 2;
set I3i1 = Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result});
set I3I2I0 = Macro (AddTo (1 -stRWNotIn {N,result}),result);
set I3I2I1 = Macro (AddTo result,(1 -stRWNotIn {N,result}));
set I3I2 = if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})));
set I = (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))));
let n be Element of NAT ; ( n = s . N implies ( (IExec (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n ) )
assume A2:
n = s . N
; ( (IExec (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n )
A3:
1 -stRWNotIn {N,result} <> 3 -rdRWNotIn {N,result}
by SFMASTR1:22;
A4:
2 -ndRWNotIn {N,result} <> 1 -stRWNotIn {N,result}
by SFMASTR1:22;
set I3 = while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))));
deffunc H1( Element of product the Object-Kind of SCM+FSA ) -> Element of NAT = abs ($1 . (2 -ndRWNotIn {N,result}));
set i2 = (2 -ndRWNotIn {N,result}) := N;
set i1 = (1 -stRWNotIn {N,result}) := (intloc 0 );
set t = IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s;
set It = Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s);
set SWt = StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s));
defpred S1[ Nat] means ex au, ne, re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . $1) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . $1) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . $1) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . $1) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) );
consider f being Function of (product the Object-Kind of SCM+FSA ),NAT such that
A5:
for x being Element of product the Object-Kind of SCM+FSA holds f . x = H1(x)
from FUNCT_2:sch 4();
A6:
N in {N,result}
by TARSKI:def 2;
then A7:
N <> 1 -stRWNotIn {N,result}
by SFMASTR1:21;
A8:
result in {N,result}
by TARSKI:def 2;
then A9:
2 -ndRWNotIn {N,result} <> result
by SFMASTR1:21;
A10:
result <> 3 -rdRWNotIn {N,result}
by A8, SFMASTR1:21;
A11:
1 -stRWNotIn {N,result} <> result
by A8, SFMASTR1:21;
A12:
N <> 3 -rdRWNotIn {N,result}
by A6, SFMASTR1:21;
A13:
N <> 2 -ndRWNotIn {N,result}
by A6, SFMASTR1:21;
A14:
2 -ndRWNotIn {N,result} <> 3 -rdRWNotIn {N,result}
by SFMASTR1:22;
A15:
for u being State of SCM+FSA st ex au, ne, re being Element of NAT st
( u . (2 -ndRWNotIn {N,result}) = au & u . (1 -stRWNotIn {N,result}) = ne & u . result = re & u . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) ) holds
ex au1, ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )
proof
let u be
State of
SCM+FSA ;
( ex au, ne, re being Element of NAT st
( u . (2 -ndRWNotIn {N,result}) = au & u . (1 -stRWNotIn {N,result}) = ne & u . result = re & u . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) ) implies ex au1, ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 ) )
given au,
ne,
re being
Element of
NAT such that A16:
u . (2 -ndRWNotIn {N,result}) = au
and A17:
u . (1 -stRWNotIn {N,result}) = ne
and A18:
u . result = re
and A19:
u . N = n
and A20:
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
;
ex au1, ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )
A21:
(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (1 -stRWNotIn {N,result}) =
(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u) . (1 -stRWNotIn {N,result})
by SCMFSA6C:3
.=
(Exec (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})),(IExec ((3 -rdRWNotIn {N,result}) := 2),u)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:7
.=
(IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (1 -stRWNotIn {N,result})
by A4, A3, SCMFSA_2:93
.=
ne
by A17, SCMFSA7B:9, SFMASTR1:22
;
A22:
(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (2 -ndRWNotIn {N,result}) =
(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:3
.=
(Exec (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})),(IExec ((3 -rdRWNotIn {N,result}) := 2),u)) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:7
.=
((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (2 -ndRWNotIn {N,result})) div ((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (3 -rdRWNotIn {N,result}))
by A14, SCMFSA_2:93
.=
(u . (2 -ndRWNotIn {N,result})) div ((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (3 -rdRWNotIn {N,result}))
by SCMFSA7B:9, SFMASTR1:22
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by SCMFSA7B:9
;
A23:
(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . result =
(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u) . result
by SCMFSA6C:3
.=
(Exec (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})),(IExec ((3 -rdRWNotIn {N,result}) := 2),u)) . result
by SCMFSA6C:7
.=
(IExec ((3 -rdRWNotIn {N,result}) := 2),u) . result
by A9, A10, SCMFSA_2:93
.=
re
by A10, A18, SCMFSA7B:9
;
A24:
(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . N =
(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u) . N
by SCMFSA6C:3
.=
(Exec (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})),(IExec ((3 -rdRWNotIn {N,result}) := 2),u)) . N
by SCMFSA6C:7
.=
(IExec ((3 -rdRWNotIn {N,result}) := 2),u) . N
by A12, A13, SCMFSA_2:93
.=
n
by A12, A19, SCMFSA7B:9
;
A25:
(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u) . (3 -rdRWNotIn {N,result}) =
(Exec (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})),(IExec ((3 -rdRWNotIn {N,result}) := 2),u)) . (3 -rdRWNotIn {N,result})
by SCMFSA6C:7
.=
((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (2 -ndRWNotIn {N,result})) mod ((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (3 -rdRWNotIn {N,result}))
by SCMFSA_2:93
.=
(u . (2 -ndRWNotIn {N,result})) mod ((IExec ((3 -rdRWNotIn {N,result}) := 2),u) . (3 -rdRWNotIn {N,result}))
by SCMFSA7B:9, SFMASTR1:22
.=
(u . (2 -ndRWNotIn {N,result})) mod 2
by SCMFSA7B:9
;
per cases
( au is even or not au is even )
;
suppose A26:
au is
even
;
ex au1, ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )reconsider ne1 =
ne + re as
Element of
NAT ;
reconsider au1 =
(u . (2 -ndRWNotIn {N,result})) div 2 as
Element of
NAT by A16, INT_1:16, INT_1:82;
take
au1
;
ex ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
ne1
;
ex re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
re
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )consider k being
Element of
NAT such that A27:
au = 2
* k
by A26, ABIAN:def 2;
A28:
(u . (2 -ndRWNotIn {N,result})) mod 2 =
((2 * k) + 0 ) mod 2
by A16, A27
.=
0 mod 2
by NAT_D:21
.=
0
by NAT_D:26
;
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec (Macro (AddTo (1 -stRWNotIn {N,result}),result)),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (2 -ndRWNotIn {N,result})
by A25, A28, SCMFSA8B:21
.=
(Exec (AddTo (1 -stRWNotIn {N,result}),result),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:6
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A4, A22, SCMFSA_2:90
;
hence
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec (Macro (AddTo (1 -stRWNotIn {N,result}),result)),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (1 -stRWNotIn {N,result})
by A25, A28, SCMFSA8B:21
.=
(Exec (AddTo (1 -stRWNotIn {N,result}),result),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:6
.=
ne1
by A21, A23, SCMFSA_2:90
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . result
by SCMFSA6C:1
.=
(IExec (Macro (AddTo (1 -stRWNotIn {N,result}),result)),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . result
by A25, A28, SCMFSA8B:21
.=
(Exec (AddTo (1 -stRWNotIn {N,result}),result),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . result
by SCMFSA6C:6
.=
re
by A11, A23, SCMFSA_2:90
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . N
by SCMFSA6C:1
.=
(IExec (Macro (AddTo (1 -stRWNotIn {N,result}),result)),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . N
by A25, A28, SCMFSA8B:21
.=
(Exec (AddTo (1 -stRWNotIn {N,result}),result),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . N
by SCMFSA6C:6
.=
n
by A7, A24, SCMFSA_2:90
;
( Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )
au1 = k
by A16, A27, NAT_D:20;
hence
Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1)))
by A20, A27, PRE_FF:22;
au1 = (u . (2 -ndRWNotIn {N,result})) div 2thus
au1 = (u . (2 -ndRWNotIn {N,result})) div 2
;
verum end; suppose A29:
not
au is
even
;
ex au1, ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )reconsider re1 =
ne + re as
Element of
NAT ;
reconsider au1 =
(u . (2 -ndRWNotIn {N,result})) div 2 as
Element of
NAT by A16, INT_1:16, INT_1:82;
take
au1
;
ex ne1, re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
ne
;
ex re1 being Element of NAT st
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
re1
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )consider k being
Element of
NAT such that A30:
au = (2 * k) + 1
by A29, ABIAN:9;
A31:
(u . (2 -ndRWNotIn {N,result})) mod 2 =
1
mod 2
by A16, A30, NAT_D:21
.=
1
by NAT_D:24
;
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec (Macro (AddTo result,(1 -stRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (2 -ndRWNotIn {N,result})
by A25, A31, SCMFSA8B:21
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:6
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A9, A22, SCMFSA_2:90
;
hence
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (2 -ndRWNotIn {N,result}) = au1
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) = ne & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . (1 -stRWNotIn {N,result}) =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec (Macro (AddTo result,(1 -stRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . (1 -stRWNotIn {N,result})
by A25, A31, SCMFSA8B:21
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:6
.=
ne
by A11, A21, SCMFSA_2:90
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result = re1 & (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . result =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . result
by SCMFSA6C:1
.=
(IExec (Macro (AddTo result,(1 -stRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . result
by A25, A31, SCMFSA8B:21
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . result
by SCMFSA6C:6
.=
re1
by A21, A23, SCMFSA_2:90
;
( (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),u) . N =
(IExec (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . N
by SCMFSA6C:1
.=
(IExec (Macro (AddTo result,(1 -stRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u)) . N
by A25, A31, SCMFSA8B:21
.=
(Exec (AddTo result,(1 -stRWNotIn {N,result})),(Initialize (IExec (((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),u))) . N
by SCMFSA6C:6
.=
n
by A1, A24, SCMFSA_2:90
;
( Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )au1 =
(2 * k) div 2
by A16, A30, NAT_2:28
.=
k
by NAT_D:20
;
hence
Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
by A20, A30, PRE_FF:21;
au1 = (u . (2 -ndRWNotIn {N,result})) div 2thus
au1 = (u . (2 -ndRWNotIn {N,result})) div 2
;
verum end;
end;
A32:
(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) . (intloc 0 ) = 1
by SCMFSA6C:3;
A33:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
given au,
ne,
re being
Element of
NAT such that A34:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) = au
and A35:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (1 -stRWNotIn {N,result}) = ne
and A36:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . result = re
and A37:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . N = n
and A38:
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
;
S1[k + 1]
A39:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (intloc 0 ) = 1
by A32, Th39;
per cases
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) > 0 or ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0 )
;
suppose A40:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) > 0
;
S1[k + 1]consider au1,
ne1,
re1 being
Element of
NAT such that A41:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . (2 -ndRWNotIn {N,result}) = au1
and A42:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . (1 -stRWNotIn {N,result}) = ne1
and A43:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . result = re1
and A44:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . N = n
and A45:
Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
and
au1 = (((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result})) div 2
by A15, A34, A35, A36, A37, A38;
take
au1
;
ex ne, re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au1)) + (re * (Fusc (au1 + 1))) )take
ne1
;
ex re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) )take
re1
;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) )A46:
DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) = DataPart (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k))
by A39, A40, Th38;
hence
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1
by A41, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne1
by A46, A42, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re1 & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re1
by A46, A43, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n
by A46, A44, SCMFSA6A:38;
Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))thus
Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
by A45;
verum end; suppose A47:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0
;
S1[k + 1]take
au
;
ex ne, re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )take
ne
;
ex re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )take
re
;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )A48:
DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) = DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)
by A47, Th37;
hence
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au
by A34, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne
by A35, A48, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . result = re
by A36, A48, SCMFSA6A:38;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )thus
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . N = n
by A37, A48, SCMFSA6A:38;
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))thus
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
by A38;
verum end;
end;
(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) . (intloc 0 ) = 1
by SCMFSA6B:35;
then A49:
DataPart (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) = DataPart (Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))
by SCMFSA8C:27;
A50:
S1[ 0 ]
proof
take au =
n;
ex ne, re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
take ne = 1;
ex re being Element of NAT st
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
take re =
0 ;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (2 -ndRWNotIn {N,result}) = au & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
A51:
(StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 = Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)
by SCMFSA_9:def 5;
hence ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (2 -ndRWNotIn {N,result}) =
(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) . (2 -ndRWNotIn {N,result})
by A49, SCMFSA6A:38
.=
(Exec ((2 -ndRWNotIn {N,result}) := N),(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s)) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:7
.=
(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . N
by SCMFSA_2:89
.=
(Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(Exec (SubFrom result,result),(Initialize s))) . N
by SCMFSA6C:9
.=
(Exec (SubFrom result,result),(Initialize s)) . N
by A7, SCMFSA_2:89
.=
(Initialize s) . N
by A1, SCMFSA_2:91
.=
au
by A2, SCMFSA6C:3
;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (1 -stRWNotIn {N,result}) = ne & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
thus ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . (1 -stRWNotIn {N,result}) =
(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) . (1 -stRWNotIn {N,result})
by A49, A51, SCMFSA6A:38
.=
(Exec ((2 -ndRWNotIn {N,result}) := N),(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:7
.=
(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . (1 -stRWNotIn {N,result})
by A4, SCMFSA_2:89
.=
(Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(Exec (SubFrom result,result),(Initialize s))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:9
.=
(Exec (SubFrom result,result),(Initialize s)) . (intloc 0 )
by SCMFSA_2:89
.=
(Initialize s) . (intloc 0 )
by SCMFSA_2:91
.=
ne
by SCMFSA6C:3
;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result = re & ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
thus ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . result =
(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) . result
by A49, A51, SCMFSA6A:38
.=
(Exec ((2 -ndRWNotIn {N,result}) := N),(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s)) . result
by SCMFSA6C:7
.=
(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . result
by A9, SCMFSA_2:89
.=
(Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(Exec (SubFrom result,result),(Initialize s))) . result
by SCMFSA6C:9
.=
(Exec (SubFrom result,result),(Initialize s)) . result
by A11, SCMFSA_2:89
.=
((Initialize s) . result) - ((Initialize s) . result)
by SCMFSA_2:91
.=
re
;
( ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N = n & Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
thus ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . 0 ) . N =
(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) . N
by A49, A51, SCMFSA6A:38
.=
(Exec ((2 -ndRWNotIn {N,result}) := N),(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s)) . N
by SCMFSA6C:7
.=
(IExec ((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))),s) . N
by A13, SCMFSA_2:89
.=
(Exec ((1 -stRWNotIn {N,result}) := (intloc 0 )),(Exec (SubFrom result,result),(Initialize s))) . N
by SCMFSA6C:9
.=
(Exec (SubFrom result,result),(Initialize s)) . N
by A7, SCMFSA_2:89
.=
(Initialize s) . N
by A1, SCMFSA_2:91
.=
n
by A2, SCMFSA6C:3
;
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
thus
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
;
verum
end;
A52:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A50, A33);
for k being Element of NAT holds
( f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) < f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) or ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0 )
proof
let k be
Element of
NAT ;
( f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) < f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) or ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0 )
consider au,
ne,
re being
Element of
NAT such that A53:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) = au
and A54:
(
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (1 -stRWNotIn {N,result}) = ne &
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . result = re &
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . N = n &
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) )
by A52;
A55:
f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) =
abs (((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}))
by A5
.=
au
by A53, ABSVALUE:def 1
;
now consider au1,
ne1,
re1 being
Element of
NAT such that A56:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . (2 -ndRWNotIn {N,result}) = au1
and
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . (1 -stRWNotIn {N,result}) = ne1
and
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . result = re1
and
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)) . N = n
and
Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
and A57:
au1 = (((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result})) div 2
by A15, A53, A54;
assume A58:
au > 0
;
f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) < f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (intloc 0 ) = 1
by A32, Th39;
then
DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) = DataPart (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k))
by A53, A58, Th38;
then A59:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1
by A56, SCMFSA6A:38;
f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) =
abs (((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) . (2 -ndRWNotIn {N,result}))
by A5
.=
au1
by A59, ABSVALUE:def 1
;
hence
f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) < f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)
by A53, A55, A58, A57, INT_1:83;
verum end;
hence
(
f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . (k + 1)) < f . ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) or
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0 )
by A53;
verum
end;
then A60:
WithVariantWhile>0 2 -ndRWNotIn {N,result},(((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))), Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)
by Def5;
then consider k being Element of NAT such that
A61:
ExitsAtWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) = k
and
A62:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) <= 0
and
for i being Element of NAT st ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . i) . (2 -ndRWNotIn {N,result}) <= 0 holds
k <= i
and
DataPart (Comput (ProgramPart ((Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) +* ((while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))) +* (Start-At 0 ,SCM+FSA )))),((Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) +* ((while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) +* ((while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)
by Def6;
A63:
DataPart (IExec (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))),(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) = DataPart ((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k)
by A60, A61, Th42;
consider au, ne, re being Element of NAT such that
A64:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (2 -ndRWNotIn {N,result}) = au
and
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . (1 -stRWNotIn {N,result}) = ne
and
A65:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . result = re
and
A66:
((StepWhile>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))),(Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s))) . k) . N = n
and
A67:
Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
by A52;
A68:
au = 0
by A62, A64;
( while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))) is_closed_on Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) & while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))) is_halting_on Initialize (IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s) )
by A60, Th34;
then A69:
( while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))) is_closed_on IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s & while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))) is_halting_on IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s )
by A49, SCMFSA8B:8;
hence (IExec (Fusc_macro N,result),s) . result =
(IExec (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))),(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) . result
by SFMASTR1:8
.=
Fusc n
by A65, A67, A68, A63, PRE_FF:17, SCMFSA6A:38
;
(IExec (Fusc_macro N,result),s) . N = n
thus (IExec (Fusc_macro N,result),s) . N =
(IExec (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))),(IExec (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)),s)) . N
by A69, SFMASTR1:8
.=
n
by A66, A63, SCMFSA6A:38
; verum