let p be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: 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; :: thesis: ( 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))) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( 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; :: thesis: au1 = (u . (2 -ndRWNotIn {N,result})) div 2
thus au1 = (u . (2 -ndRWNotIn {N,result})) div 2 ; :: thesis: verum
end;
suppose A29: au is odd ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( 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; :: thesis: au1 = (u . (2 -ndRWNotIn {N,result})) div 2
thus au1 = (u . (2 -ndRWNotIn {N,result})) div 2 ; :: thesis: verum
end;
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; :: thesis: ( 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))) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1)))
thus Fusc n = (ne1 * (Fusc au1)) + (re1 * (Fusc (au1 + 1))) by A45; :: thesis: 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 ; :: thesis: S1[k + 1]
take au ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: ( ((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; :: thesis: Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
thus Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) by A38; :: thesis: verum
end;
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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( ((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 ;
:: thesis: ( ((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 ; :: thesis: ( ((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 ; :: thesis: ( ((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 ; :: thesis: Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1)))
thus Fusc n = (ne * (Fusc au)) + (re * (Fusc (au + 1))) ; :: thesis: 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; :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ;
:: thesis: (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 ; :: thesis: verum