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})));
reconsider I3I2 = if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result}))))) as really-closed Program of ;
reconsider I = (((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" I3I2 as really-closed MacroInstruction of SCM+FSA ;
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 SCMFSA_M:26;
A4:
2 -ndRWNotIn {N,result} <> 1 -stRWNotIn {N,result}
by SCMFSA_M:26;
set I3 = while>0 ((2 -ndRWNotIn {N,result}),I);
deffunc H1( Element of product (the_Values_of SCM+FSA)) -> Element of NAT = |.($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}),I,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}),I));
defpred S1[ Nat] means ex au, ne, re being Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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_Values_of SCM+FSA)),NAT such that
A5:
for x being Element of product (the_Values_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 SCMFSA_M:25;
A8:
result in {N,result}
by TARSKI:def 2;
then A9:
2 -ndRWNotIn {N,result} <> result
by SCMFSA_M:25;
A10:
result <> 3 -rdRWNotIn {N,result}
by A8, SCMFSA_M:25;
A11:
1 -stRWNotIn {N,result} <> result
by A8, SCMFSA_M:25;
A12:
N <> 3 -rdRWNotIn {N,result}
by A6, SCMFSA_M:25;
A13:
N <> 2 -ndRWNotIn {N,result}
by A6, SCMFSA_M:25;
A14:
2 -ndRWNotIn {N,result} <> 3 -rdRWNotIn {N,result}
by SCMFSA_M:26;
A15:
for u being State of SCM+FSA
for h being Instruction-Sequence of SCM+FSA st ex au, ne, re being 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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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
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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 SCMFSA_M:37
.=
(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, SCMFSA_M:26
;
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 SCMFSA_M:37
.=
(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, SCMFSA_M:26
.=
(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 SCMFSA_M:37
.=
(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 SCMFSA_M:37
.=
(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, SCMFSA_M:26
.=
(u . (2 -ndRWNotIn {N,result})) mod 2
by SCMFSA7B:3
;
per cases
( au is even or au is odd )
;
suppose A26:
au is
even
;
ex au1, ne1, re1 being Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 by ORDINAL1:def 12;
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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
re
;
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re & (IExec (I,h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )consider k being
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 (I,h,u)) . (2 -ndRWNotIn {N,result}) =
(IExec (I3I2,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
.=
(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
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A4, A22, SCMFSA_2:64
;
hence
(IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1
;
( (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re & (IExec (I,h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) =
(IExec (I3I2,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
.=
(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
.=
ne1
by A21, A23, SCMFSA_2:64
;
( (IExec (I,h,u)) . result = re & (IExec (I,h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . result =
(IExec (I3I2,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
.=
(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
.=
re
by A11, A23, SCMFSA_2:64
;
( (IExec (I,h,u)) . N = n & Fusc n = (ne1 * (Fusc au1)) + (re * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . N =
(IExec (I3I2,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
.=
(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
.=
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:18;
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:
au is
odd
;
ex au1, ne1, re1 being Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 by ORDINAL1:def 12;
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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne1 & (IExec (I,h,u)) . result = re1 & (IExec (I,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 Nat st
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne & (IExec (I,h,u)) . result = re1 & (IExec (I,h,u)) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )take
re1
;
( (IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1 & (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne & (IExec (I,h,u)) . result = re1 & (IExec (I,h,u)) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )consider k being
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 (I,h,u)) . (2 -ndRWNotIn {N,result}) =
(IExec (I3I2,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
.=
(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
.=
(u . (2 -ndRWNotIn {N,result})) div 2
by A9, A22, SCMFSA_2:64
;
hence
(IExec (I,h,u)) . (2 -ndRWNotIn {N,result}) = au1
;
( (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) = ne & (IExec (I,h,u)) . result = re1 & (IExec (I,h,u)) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . (1 -stRWNotIn {N,result}) =
(IExec (I3I2,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
.=
(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
.=
ne
by A11, A21, SCMFSA_2:64
;
( (IExec (I,h,u)) . result = re1 & (IExec (I,h,u)) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . result =
(IExec (I3I2,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
.=
(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
.=
re1
by A21, A23, SCMFSA_2:64
;
( (IExec (I,h,u)) . N = n & Fusc n = (ne * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) & au1 = (u . (2 -ndRWNotIn {N,result})) div 2 )thus (IExec (I,h,u)) . N =
(IExec (I3I2,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
.=
(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
.=
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:18
;
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 SCMFSA_M:9;
A33:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
given au,
ne,
re being
Nat such that A34:
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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, Th33;
per cases
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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
Nat such that A41:
(IExec (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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 (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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 (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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 (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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 Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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 Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k)))
by A39, A40, Th32;
hence
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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, SCMFSA_M:2;
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}),I,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 Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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 Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k)
by A47, Th31;
hence
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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, SCMFSA_M:2;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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, SCMFSA_M:2;
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 SCMFSA_M:19;
A50:
S1[ 0 ]
proof
take au =
n;
ex ne, re being Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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 Nat st
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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, SCMFSA_M:2
.=
(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, SCMFSA_M:37
;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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, SCMFSA_M:2
.=
(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 SCMFSA_M:9
;
( ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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, SCMFSA_M:2
.=
(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}),I,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}),I,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, SCMFSA_M:2
.=
(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, SCMFSA_M:37
;
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 Nat holds S1[k]
from NAT_1:sch 2(A50, A33);
for k being Nat holds
( f . ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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
Nat;
( f . ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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
Nat such that A53:
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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 ( au > 0 implies f . ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k) )consider au1,
ne1,
re1 being
Nat such that A56:
(IExec (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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 (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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 (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k))) . result = re1
and
(IExec (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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, Th33;
then
DataPart ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 ((2 -ndRWNotIn {N,result}),I))),((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k)))
by A53, A58, Th32;
then A59:
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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, SCMFSA_M:2;
f . ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . (k + 1)) =
|.(((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I,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}),I,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},I, Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s)),p
;
then consider k being Nat such that
A61:
ExitsAtWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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 Nat st ((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I))),(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}),I))),(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}),I,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}),I)),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}),I,p,(Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s))))) . k)
by A60, A61, Th36;
consider au, ne, re being Nat such that
A64:
((StepWhile>0 ((2 -ndRWNotIn {N,result}),I,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}),I,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}),I,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}),I,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}),I) is_halting_on Initialized (IExec ((((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)),p,s)),p
by A60, Th28;
then A69:
while>0 ((2 -ndRWNotIn {N,result}),I) 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}),I)),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, SCMFSA_M:2
;
(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}),I)),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, SCMFSA_M:2
; verum