let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let C be bool-correct 4,1 integer image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let G be basic GeneratorSystem over S,X,T; :: thesis: for A being IfWhileAlgebra of the generators of G
for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let A be IfWhileAlgebra of the generators of G; :: thesis: for I being integer SortSymbol of S
for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let I be integer SortSymbol of S; :: thesis: for b being pure Element of the generators of G . the bool-sort of S
for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: for t being Element of T,I
for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let t be Element of T,I; :: thesis: for s being Element of C -States the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let s be Element of C -States the generators of G; :: thesis: for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is C -supported & f in C -Execution (A,b,(\false C)) holds
( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is C -supported & f in C -Execution (A,b,(\false C)) implies ( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) ) )
assume A1: ( G is C -supported & f in C -Execution (A,b,(\false C)) ) ; :: thesis: ( ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2 & ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
reconsider b0 = @ b as Element of G, the bool-sort of S by AOFA_A00:def 22;
A2: ( (\2 (T,I)) value_at (C,s) = 2 & (\0 (T,I)) value_at (C,s) = 0 ) by Th36, Th40;
then A3: (t value_at (C,s)) mod ((\2 (T,I)) value_at (C,s)) = (t value_at (C,s)) mod 2 by Th64;
then A4: leq (((t value_at (C,s)) mod ((\2 (T,I)) value_at (C,s))),((\0 (T,I)) value_at (C,s))) = IFGT (((t value_at (C,s)) mod 2),0,FALSE,TRUE) by A2, AOFA_A00:55;
reconsider Z = IFGT (((t value_at (C,s)) mod 2),0,FALSE,TRUE) as boolean object ;
A5: ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = ((succ (s,b0,((\not (leq ((t mod (\2 (T,I))),(\0 (T,I))))) value_at (C,s)))) . the bool-sort of S) . b by A1, AOFA_A00:def 28
.= (\not (leq ((t mod (\2 (T,I))),(\0 (T,I))))) value_at (C,s) by A1, AOFA_A00:def 27
.= \not ((leq ((t mod (\2 (T,I))),(\0 (T,I)))) value_at (C,s)) by Th31
.= \not (leq (((t mod (\2 (T,I))) value_at (C,s)),((\0 (T,I)) value_at (C,s)))) by Th45
.= \not (leq (((t value_at (C,s)) mod ((\2 (T,I)) value_at (C,s))),((\0 (T,I)) value_at (C,s)))) by Th44
.= 'not' Z by A4, AOFA_A00:def 32 ;
hereby :: thesis: ( ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2 & ( for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z ) ) )
per cases ( (t value_at (C,s)) mod 2 = 0 or (t value_at (C,s)) mod 2 = 1 ) by PRE_FF:6;
suppose A6: (t value_at (C,s)) mod 2 = 0 ; :: thesis: ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2
hence ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = 'not' TRUE by A5, XXREAL_0:def 11
.= (t value_at (C,s)) mod 2 by A6 ;
:: thesis: verum
end;
suppose A7: (t value_at (C,s)) mod 2 = 1 ; :: thesis: ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = (t value_at (C,s)) mod 2
hence ((f . (s,(t is_odd (b,A)))) . the bool-sort of S) . b = 'not' FALSE by A5, XXREAL_0:def 11
.= (t value_at (C,s)) mod 2 by A7 ;
:: thesis: verum
end;
end;
end;
A8: ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((succ (s,b0,((leq ((t mod (\2 (T,I))),(\0 (T,I)))) value_at (C,s)))) . the bool-sort of S) . b by A1, AOFA_A00:def 28
.= (leq ((t mod (\2 (T,I))),(\0 (T,I)))) value_at (C,s) by A1, AOFA_A00:def 27
.= leq (((t mod (\2 (T,I))) value_at (C,s)),((\0 (T,I)) value_at (C,s))) by Th45
.= leq (((t value_at (C,s)) mod ((\2 (T,I)) value_at (C,s))),((\0 (T,I)) value_at (C,s))) by Th44
.= IFGT (((t value_at (C,s)) mod 2),0,FALSE,TRUE) by A3, A2, AOFA_A00:55 ;
hereby :: thesis: for z being pure Element of the generators of G . I holds
( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z )
per cases ( (t value_at (C,s)) mod 2 = 0 or (t value_at (C,s)) mod 2 = 1 ) by PRE_FF:6;
suppose A9: (t value_at (C,s)) mod 2 = 0 ; :: thesis: ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2
hence ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = (0 + 1) mod 2 by Th1, A8, XXREAL_0:def 11
.= ((t value_at (C,s)) + 1) mod 2 by A9, Th1, NAT_D:66 ;
:: thesis: verum
end;
suppose A10: (t value_at (C,s)) mod 2 = 1 ; :: thesis: ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = ((t value_at (C,s)) + 1) mod 2
hence ((f . (s,(t is_even (b,A)))) . the bool-sort of S) . b = (1 + 1) mod 2 by Th1, A8, XXREAL_0:def 11
.= ((t value_at (C,s)) + 1) mod 2 by A10, Th1, NAT_D:66 ;
:: thesis: verum
end;
end;
end;
let z be pure Element of the generators of G . I; :: thesis: ( ((f . (s,(t is_odd (b,A)))) . I) . z = (s . I) . z & ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z )
A11: I <> the bool-sort of S by AOFA_A00:53;
b in (FreeGen T) . the bool-sort of S by Def4;
then vf (@ b) = the bool-sort of S -singleton b by AOFA_A00:41;
then A12: z nin (vf (@ b)) . I by A11, AOFA_A00:6;
A13: z in (FreeGen T) . I by Def4;
thus ((f . (s,(t is_odd (b,A)))) . I) . z = ((succ (s,b0,((\not (leq ((t mod (\2 (T,I))),(\0 (T,I))))) value_at (C,s)))) . I) . z by A1, AOFA_A00:def 28
.= (s . I) . z by A1, A11, A12, A13, AOFA_A00:def 27 ; :: thesis: ((f . (s,(t is_even (b,A)))) . I) . z = (s . I) . z
thus ((f . (s,(t is_even (b,A)))) . I) . z = ((succ (s,b0,((leq ((t mod (\2 (T,I))),(\0 (T,I)))) value_at (C,s)))) . I) . z by A1, AOFA_A00:def 28
.= (s . I) . z by A1, A11, A12, A13, AOFA_A00:def 27 ; :: thesis: verum