let p be Instruction-Sequence of SCM+FSA; for s being 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)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n )
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)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,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)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n ) )
assume A1:
N <> result
; for n being Element of NAT st n = s . N holds
( (IExec ((Fusc_macro (N,result)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,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)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n ) )
assume A2:
n = s . N
; ( (IExec ((Fusc_macro (N,result)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n )
A3:
1 -stRWNotIn {N,result} <> 3 -rdRWNotIn {N,result}
by SFMASTR1:21;
A4:
2 -ndRWNotIn {N,result} <> 1 -stRWNotIn {N,result}
by SFMASTR1:21;
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)),p,s);
set q = p;
set It = Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))));
set PWt = p +* (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})))))))));
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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:20;
A8:
result in {N,result}
by TARSKI:def 2;
then A9:
2 -ndRWNotIn {N,result} <> result
by SFMASTR1:20;
A10:
result <> 3 -rdRWNotIn {N,result}
by A8, SFMASTR1:20;
A11:
1 -stRWNotIn {N,result} <> result
by A8, SFMASTR1:20;
A12:
N <> 3 -rdRWNotIn {N,result}
by A6, SFMASTR1:20;
A13:
N <> 2 -ndRWNotIn {N,result}
by A6, SFMASTR1:20;
A14:
2 -ndRWNotIn {N,result} <> 3 -rdRWNotIn {N,result}
by SFMASTR1:21;
A15:
for u being State of SCM+FSA
for h being Instruction-Sequence 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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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;
for h being Instruction-Sequence 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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )let h be
Instruction-Sequence 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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )
A21:
(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))) . (1 -stRWNotIn {N,result}) =
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)) . (1 -stRWNotIn {N,result})
by SCMFSA6C:3
.=
(Exec ((Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:6
.=
(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (1 -stRWNotIn {N,result})
by A4, A3, SCMFSA_2:67
.=
ne
by A17, SCMFSA7B:3, SFMASTR1:21
;
A22:
(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))) . (2 -ndRWNotIn {N,result}) =
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:3
.=
(Exec ((Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:6
.=
((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (2 -ndRWNotIn {N,result})) div ((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (3 -rdRWNotIn {N,result}))
by A14, SCMFSA_2:67
.=
(u . (2 -ndRWNotIn {N,result})) div ((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (3 -rdRWNotIn {N,result}))
by SCMFSA7B:3, SFMASTR1:21
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by SCMFSA7B:3
;
A23:
(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))) . result =
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)) . result
by SCMFSA6C:3
.=
(Exec ((Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)))) . result
by SCMFSA6C:6
.=
(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . result
by A9, A10, SCMFSA_2:67
.=
re
by A10, A18, SCMFSA7B:3
;
A24:
(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))) . N =
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)) . N
by SCMFSA6C:3
.=
(Exec ((Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)))) . N
by SCMFSA6C:6
.=
(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . N
by A12, A13, SCMFSA_2:67
.=
n
by A12, A19, SCMFSA7B:3
;
A25:
(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)) . (3 -rdRWNotIn {N,result}) =
(Exec ((Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))),(IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)))) . (3 -rdRWNotIn {N,result})
by SCMFSA6C:6
.=
((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (2 -ndRWNotIn {N,result})) mod ((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (3 -rdRWNotIn {N,result}))
by SCMFSA_2:67
.=
(u . (2 -ndRWNotIn {N,result})) mod ((IExec (((3 -rdRWNotIn {N,result}) := 2),h,u)) . (3 -rdRWNotIn {N,result}))
by SCMFSA7B:3, SFMASTR1:21
.=
(u . (2 -ndRWNotIn {N,result})) mod 2
by SCMFSA7B:3
;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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:3, INT_1:55;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
by A25, A28, SCMFSA8B:18
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:5
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (2 -ndRWNotIn {N,result})
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A4, A22, SCMFSA_2:64
;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
by A25, A28, SCMFSA8B:18
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:5
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (1 -stRWNotIn {N,result})
.=
ne1
by A21, A23, SCMFSA_2:64
;
( (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}))))))),h,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}))))))),h,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}))))))),h,u)) . result =
(IExec ((if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
by A25, A28, SCMFSA8B:18
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . result
by SCMFSA6C:5
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . result
.=
re
by A11, A23, SCMFSA_2:64
;
( (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}))))))),h,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}))))))),h,u)) . N =
(IExec ((if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
by A25, A28, SCMFSA8B:18
.=
(IExec ((Macro (AddTo ((1 -stRWNotIn {N,result}),result))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . N
by SCMFSA6C:5
.=
(Exec ((AddTo ((1 -stRWNotIn {N,result}),result)),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . N
.=
n
by A7, A24, SCMFSA_2:64
;
( 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:20;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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:3, INT_1:55;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
by A25, A31, SCMFSA8B:18
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (2 -ndRWNotIn {N,result})
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:5
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (2 -ndRWNotIn {N,result})
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A9, A22, SCMFSA_2:64
;
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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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}))))))),h,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})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
by A25, A31, SCMFSA8B:18
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . (1 -stRWNotIn {N,result})
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:5
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . (1 -stRWNotIn {N,result})
.=
ne
by A11, A21, SCMFSA_2:64
;
( (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}))))))),h,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}))))))),h,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}))))))),h,u)) . result =
(IExec ((if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
by A25, A31, SCMFSA8B:18
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . result
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . result
by SCMFSA6C:5
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . result
.=
re1
by A21, A23, SCMFSA_2:64
;
( (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}))))))),h,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}))))))),h,u)) . N =
(IExec ((if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
by SCMFSA6C:1
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
by A25, A31, SCMFSA8B:18
.=
(IExec ((Macro (AddTo (result,(1 -stRWNotIn {N,result})))),h,(IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u)))) . N
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . N
by SCMFSA6C:5
.=
(Exec ((AddTo (result,(1 -stRWNotIn {N,result}))),(Initialized (IExec ((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))),h,u))))) . N
.=
n
by A1, A24, SCMFSA_2:64
;
( 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:26
.=
k
by NAT_D:20
;
hence
Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
by A20, A30, PRE_FF:19;
au1 = (u . (2 -ndRWNotIn {N,result})) div 2thus
au1 = (u . (2 -ndRWNotIn {N,result})) div 2
;
verum end;
end;
A32:
(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))) . (intloc 0) = 1
by SCMFSA6A:38;
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1
by A41, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne1
by A46, A42, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . result = re1
by A46, A43, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . N = n
by A46, A44, SCMFSA6A:7;
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au
by A34, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . (1 -stRWNotIn {N,result}) = ne
by A35, A48, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . result = re
by A36, A48, SCMFSA6A:7;
( ((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . N = n
by A37, A48, SCMFSA6A:7;
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)),p,s)) . (intloc 0) = 1
by SCMFSA6B:11;
then A49:
DataPart (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)) = DataPart (Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)))
by SCMFSA8C:7;
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . 0 = Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . 0) . (2 -ndRWNotIn {N,result}) =
(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)) . (2 -ndRWNotIn {N,result})
by A49, SCMFSA6A:7
.=
(Exec (((2 -ndRWNotIn {N,result}) := N),(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (2 -ndRWNotIn {N,result})
by SCMFSA6C:6
.=
(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N
by SCMFSA_2:63
.=
(Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(Exec ((SubFrom (result,result)),(Initialized s))))) . N
by SCMFSA6C:8
.=
(Exec ((SubFrom (result,result)),(Initialized s))) . N
by A7, SCMFSA_2:63
.=
(Initialized s) . N
by A1, SCMFSA_2:65
.=
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . 0) . (1 -stRWNotIn {N,result}) =
(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)) . (1 -stRWNotIn {N,result})
by A49, A51, SCMFSA6A:7
.=
(Exec (((2 -ndRWNotIn {N,result}) := N),(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:6
.=
(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . (1 -stRWNotIn {N,result})
by A4, SCMFSA_2:63
.=
(Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(Exec ((SubFrom (result,result)),(Initialized s))))) . (1 -stRWNotIn {N,result})
by SCMFSA6C:8
.=
(Exec ((SubFrom (result,result)),(Initialized s))) . (intloc 0)
by SCMFSA_2:63
.=
(Initialized s) . (intloc 0)
by SCMFSA_2:65
.=
ne
by 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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . 0) . result =
(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)) . result
by A49, A51, SCMFSA6A:7
.=
(Exec (((2 -ndRWNotIn {N,result}) := N),(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . result
by SCMFSA6C:6
.=
(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . result
by A9, SCMFSA_2:63
.=
(Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(Exec ((SubFrom (result,result)),(Initialized s))))) . result
by SCMFSA6C:8
.=
(Exec ((SubFrom (result,result)),(Initialized s))) . result
by A11, SCMFSA_2:63
.=
((Initialized s) . result) - ((Initialized s) . result)
by SCMFSA_2:65
.=
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . 0) . N =
(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)) . N
by A49, A51, SCMFSA6A:7
.=
(Exec (((2 -ndRWNotIn {N,result}) := N),(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)))) . N
by SCMFSA6C:6
.=
(IExec (((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))),p,s)) . N
by A13, SCMFSA_2:63
.=
(Exec (((1 -stRWNotIn {N,result}) := (intloc 0)),(Exec ((SubFrom (result,result)),(Initialized s))))) . N
by SCMFSA6C:8
.=
(Exec ((SubFrom (result,result)),(Initialized s))) . N
by A7, SCMFSA_2:63
.=
(Initialized s) . N
by A1, SCMFSA_2:65
.=
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),(p +* (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})))))))))),((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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) . (2 -ndRWNotIn {N,result}) = au1
by A56, SCMFSA6A:7;
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k)
by A53, A55, A58, A57, INT_1:56;
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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})))))), Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)),p
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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . i) . (2 -ndRWNotIn {N,result}) <= 0 holds
k <= i
and
DataPart (Comput ((p +* (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})))))))))),(Initialize (Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)))),(LifeSpan ((p +* (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})))))))))),(Initialize (Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))))),p,(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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}))))))),p,(Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,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 Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)),p & 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 Initialized (IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)),p )
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)),p,s),p & 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)),p,s),p )
by A49, SCMFSA8B:5;
hence (IExec ((Fusc_macro (N,result)),p,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}))))))))),p,(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)))) . result
by SFMASTR1:7
.=
Fusc n
by A65, A67, A68, A63, PRE_FF:15, SCMFSA6A:7
;
(IExec ((Fusc_macro (N,result)),p,s)) . N = n
thus (IExec ((Fusc_macro (N,result)),p,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}))))))))),p,(IExec ((((SubFrom (result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)),p,s)))) . N
by A69, SFMASTR1:7
.=
n
by A66, A63, SCMFSA6A:7
; verum