| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (398 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (328 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
Global Index
A
AltSpec [definition, in FlipG]alt_mono_is_fg [lemma, in FlipG]
alt_mono_unique [lemma, in FlipG]
alt_mono_bound [lemma, in FlipG]
alt_5 [lemma, in FlipG]
alt_4 [lemma, in FlipG]
alt_bound' [lemma, in FlipG]
alt_bound [lemma, in FlipG]
alt_spec_oups [lemma, in FlipG]
alt_spec_fg [lemma, in FlipG]
B
Binary [definition, in FunG]binary_rchild_is_binary [lemma, in FlipG]
binary_lchild_is_unary [lemma, in FlipG]
binary_rchild_is_unary [lemma, in FunG]
binary_lchild_is_binary [lemma, in FunG]
binary_carac2 [lemma, in FunG]
binary_carac1 [lemma, in FunG]
D
d [definition, in FlipG]d [definition, in FunG]
Dcons [constructor, in DeltaList]
decomp_complete' [lemma, in Fib]
decomp_complete [lemma, in Fib]
decomp_unique [lemma, in Fib]
decomp_exists [lemma, in Fib]
decomp_unique_rev [lemma, in Fib]
decomp_exists_rev [lemma, in Fib]
decomp_max [lemma, in Fib]
decomp_binary_iff [lemma, in FunG]
decomp_unary_iff [lemma, in FunG]
decomp_binary [lemma, in FunG]
decomp_unary [lemma, in FunG]
decomp_rchild [lemma, in FunG]
Delta [inductive, in DeltaList]
DeltaList [library]
DeltaRev [inductive, in DeltaList]
DeltaRev_rev [lemma, in DeltaList]
DeltaRev_app_inv [lemma, in DeltaList]
DeltaRev_app [lemma, in DeltaList]
DeltaRev_alt [lemma, in DeltaList]
delta_eqn [lemma, in FlipG]
delta_bc [lemma, in FlipG]
delta_c [lemma, in FlipG]
delta_b [lemma, in FlipG]
delta_a [lemma, in FlipG]
delta_0_1 [lemma, in FlipG]
Delta_rev [lemma, in DeltaList]
Delta_app_inv [lemma, in DeltaList]
Delta_app [lemma, in DeltaList]
Delta_seq [lemma, in DeltaList]
Delta_pred [lemma, in DeltaList]
Delta_map [lemma, in DeltaList]
Delta_21_S [lemma, in DeltaList]
Delta_low_hd [lemma, in DeltaList]
Delta_nz [lemma, in DeltaList]
Delta_21 [lemma, in DeltaList]
Delta_more [lemma, in DeltaList]
Delta_inv [lemma, in DeltaList]
Delta_alt [lemma, in DeltaList]
Delta_odds [lemma, in Fib]
Delta_evens [lemma, in Fib]
delta_eqn [lemma, in FunG]
delta_b [lemma, in FunG]
delta_a [lemma, in FunG]
delta_0_1 [lemma, in FunG]
depth [definition, in FunG]
depth_carac [lemma, in FunG]
depth_0 [lemma, in FunG]
depth_Sfib [lemma, in FunG]
depth_fib [lemma, in FunG]
depth_mono [lemma, in FunG]
depth_minimal [lemma, in FunG]
depth_correct [lemma, in FunG]
depth_eqn [lemma, in FunG]
depth_SS [lemma, in FunG]
Dnil [constructor, in DeltaList]
Done [constructor, in DeltaList]
DRcons [constructor, in DeltaList]
DRnil [constructor, in DeltaList]
DRone [constructor, in DeltaList]
E
Even [definition, in Fib]EvenHigh_pred_ThreeOdd [lemma, in Fib]
EvenHigh_pred_Odd [lemma, in Fib]
evens [definition, in Fib]
evens_in [lemma, in Fib]
evens_S [lemma, in Fib]
Even_not_ThreeOdd [lemma, in Fib]
Even_12 [lemma, in Fib]
Even_xor_Odd [lemma, in Fib]
Even_or_Odd [lemma, in Fib]
Even_gP [lemma, in FunG]
Even_g [lemma, in FunG]
F
FD [inductive, in FlipG]FD_step [lemma, in FlipG]
FD_unique [lemma, in FlipG]
FD_lt [lemma, in FlipG]
FD_nz [lemma, in FlipG]
FD_le [lemma, in FlipG]
FD_c [constructor, in FlipG]
FD_b [constructor, in FlipG]
FD_a [constructor, in FlipG]
FD_4 [constructor, in FlipG]
FD_3 [constructor, in FlipG]
FD_2 [constructor, in FlipG]
FD_1 [constructor, in FlipG]
FD_0 [constructor, in FlipG]
fg [definition, in FlipG]
fg_alt_eqn [lemma, in FlipG]
fg_c_inv [lemma, in FlipG]
fg_c [lemma, in FlipG]
fg_b [lemma, in FlipG]
fg_a [lemma, in FlipG]
fg_unique [lemma, in FlipG]
fg_implements_FD [lemma, in FlipG]
fg_g_step [lemma, in FlipG]
fg_g [lemma, in FlipG]
fg_g_aux3 [lemma, in FlipG]
fg_g_aux2 [lemma, in FlipG]
fg_g_aux1 [lemma, in FlipG]
fg_g_aux0 [lemma, in FlipG]
fg_g_eq_inv [lemma, in FlipG]
fg_g_S_inv [lemma, in FlipG]
fg_children [lemma, in FlipG]
fg_onto_eqn' [lemma, in FlipG]
fg_onto_eqn [lemma, in FlipG]
fg_multary_binary [lemma, in FlipG]
fg_eqn_unique [lemma, in FlipG]
fg_eqn [lemma, in FlipG]
fg_inv [lemma, in FlipG]
fg_max_two_antecedents [lemma, in FlipG]
fg_nonflat [lemma, in FlipG]
fg_onto [lemma, in FlipG]
fg_lt [lemma, in FlipG]
fg_le [lemma, in FlipG]
fg_fix [lemma, in FlipG]
fg_nz [lemma, in FlipG]
fg_0_inv [lemma, in FlipG]
fg_nonzero [lemma, in FlipG]
fg_lipschitz [lemma, in FlipG]
fg_mono [lemma, in FlipG]
fg_mono_S [lemma, in FlipG]
fg_step [lemma, in FlipG]
fg_Sfib' [lemma, in FlipG]
fg_fib' [lemma, in FlipG]
fg_Sfib [lemma, in FlipG]
fg_fib [lemma, in FlipG]
fg_depth [lemma, in FlipG]
fib [definition, in Fib]
Fib [library]
fib_inv [lemma, in Fib]
fib_le_id [lemma, in Fib]
fib_lt_inv [lemma, in Fib]
fib_inj [lemma, in Fib]
fib_mono [lemma, in Fib]
fib_mono_S [lemma, in Fib]
fib_lt [lemma, in Fib]
fib_lt_S [lemma, in Fib]
fib_0_inv [lemma, in Fib]
fib_nz [lemma, in Fib]
fib_S_nz [lemma, in Fib]
fib_eqn' [lemma, in Fib]
fib_eqn [lemma, in Fib]
flip [definition, in FlipG]
FlipG [library]
flip_pred [lemma, in FlipG]
flip_S [lemma, in FlipG]
flip_high [lemma, in FlipG]
flip_low [lemma, in FlipG]
flip_swap [lemma, in FlipG]
flip_eq [lemma, in FlipG]
flip_flip [lemma, in FlipG]
flip_fib [lemma, in FlipG]
flip_Sfib [lemma, in FlipG]
flip_eqn [lemma, in FlipG]
flip_eqn0 [lemma, in FlipG]
flip_depth [lemma, in FlipG]
Four [definition, in Fib]
Four_pred_Three [lemma, in Fib]
FunG [library]
FunG_prog [library]
G
g [definition, in FunG_prog]g [definition, in FunG]
G [inductive, in FunG]
GD [inductive, in FunG]
GD_unique [lemma, in FunG]
GD_b' [constructor, in FunG]
GD_b [constructor, in FunG]
GD_a [constructor, in FunG]
GD_1 [constructor, in FunG]
GD_0 [constructor, in FunG]
GS [constructor, in FunG]
GS_inv [lemma, in FunG]
g_le_fg [lemma, in FlipG]
g_phi [lemma, in Phi]
g_tau [lemma, in Phi]
g_spec [definition, in FunG_prog]
g_implements_GD [lemma, in FunG]
g_alt_def [lemma, in FunG]
g_pred_pred_fib [lemma, in FunG]
g_pred_fib_even [lemma, in FunG]
g_pred_fib_odd [lemma, in FunG]
g_not_Two [lemma, in FunG]
g_Two_iff [lemma, in FunG]
g_Two [lemma, in FunG]
g_Low' [lemma, in FunG]
g_Low [lemma, in FunG]
g_sumfib_rev [lemma, in FunG]
g_sumfib' [lemma, in FunG]
g_sumfib [lemma, in FunG]
g_depth [lemma, in FunG]
g_alt_eqn [lemma, in FunG]
g_lchild [lemma, in FunG]
g_children [lemma, in FunG]
g_Sfib' [lemma, in FunG]
g_Sfib [lemma, in FunG]
g_fib' [lemma, in FunG]
g_fib [lemma, in FunG]
g_onto_eqn [lemma, in FunG]
g_onto [lemma, in FunG]
g_inv [lemma, in FunG]
g_max_two_antecedents [lemma, in FunG]
g_div2_le [lemma, in FunG]
g_double_le [lemma, in FunG]
g_SS [lemma, in FunG]
g_nonflat' [lemma, in FunG]
g_nonflat [lemma, in FunG]
g_prev [lemma, in FunG]
g_next [lemma, in FunG]
g_lt [lemma, in FunG]
g_le [lemma, in FunG]
g_fix [lemma, in FunG]
g_nz [lemma, in FunG]
g_0_inv [lemma, in FunG]
g_nonzero [lemma, in FunG]
g_lipschitz [lemma, in FunG]
g_mono [lemma, in FunG]
g_mono_S [lemma, in FunG]
g_step [lemma, in FunG]
g_unique [lemma, in FunG]
g_S [lemma, in FunG]
g_eqn [lemma, in FunG]
g_0 [lemma, in FunG]
g_complete [lemma, in FunG]
g_correct [lemma, in FunG]
g_spec [definition, in FunG]
G_fun [lemma, in FunG]
G_rec [lemma, in FunG]
G_le [lemma, in FunG]
G0 [constructor, in FunG]
G1 [lemma, in FunG]
H
HeadLeEven [definition, in Fib]High [definition, in Fib]
High_succ_Two [lemma, in Fib]
High_not_ThreeOdd' [lemma, in Fib]
High_not_ThreeOdd [lemma, in Fib]
High_not_Three' [lemma, in Fib]
High_not_Three [lemma, in Fib]
High_12 [lemma, in Fib]
High_Sg [lemma, in FunG]
High_g [lemma, in FunG]
I
IHeq [definition, in FlipG]IHsucc [definition, in FlipG]
int_part_le [lemma, in Phi]
int_frac [lemma, in Phi]
int_part_carac [lemma, in Phi]
int_part_iff [lemma, in Phi]
in_seq [lemma, in DeltaList]
iter_S [lemma, in FunG]
L
lchild [definition, in FlipG]lchild [definition, in FunG]
lchild_rchild [lemma, in FlipG]
lchild_leftmost' [lemma, in FlipG]
lchild_leftmost [lemma, in FlipG]
lchild'_alt [lemma, in FlipG]
leftmost_son_is_binary [lemma, in FunG]
Low [definition, in Fib]
Low_le [lemma, in Fib]
Low_12 [lemma, in Fib]
Low_21 [lemma, in Fib]
Low_unique [lemma, in Fib]
Low_nz [lemma, in Fib]
Low_exists [lemma, in Fib]
M
map_S_pred [lemma, in FunG]map_ext_in [lemma, in FunG]
monotone_equiv [lemma, in FlipG]
Multary [definition, in FunG]
multary_flip [lemma, in FlipG]
multary_binary [lemma, in FunG]
N
norm [definition, in Fib]norm_le [lemma, in Fib]
norm_hd [lemma, in Fib]
norm_ok' [lemma, in Fib]
norm_ok [lemma, in Fib]
norm_sum [lemma, in Fib]
norm_spec [lemma, in Fib]
nothing_new [lemma, in FunG_prog]
O
Odd [definition, in Fib]odds [definition, in Fib]
odds_in [lemma, in Fib]
Odd_pred_Two [lemma, in Fib]
Odd_succ_Even [lemma, in Fib]
Odd_12 [lemma, in Fib]
Odd_gP [lemma, in FunG]
Odd_g [lemma, in FunG]
oups [definition, in FlipG]
oups_alt_eqn [lemma, in FlipG]
oups_def [lemma, in FlipG]
P
phi [definition, in Phi]Phi [library]
phi_nz [lemma, in Phi]
prime_irr [lemma, in Phi]
prime_5 [lemma, in Phi]
R
rchild [definition, in FlipG]rchild [definition, in FunG]
rchild_lchild [lemma, in FlipG]
rightmost_son_is_binary [lemma, in FlipG]
rightmost_child_carac [lemma, in FlipG]
rightmost_child_carac [lemma, in FunG]
S
seq_end [lemma, in Fib]seq_S [lemma, in Fib]
sqrt5_irr [lemma, in Phi]
sumfib [definition, in Fib]
sumfib_odds [lemma, in Fib]
sumfib_evens [lemma, in Fib]
sumfib_0 [lemma, in Fib]
sumfib_rev [lemma, in Fib]
sumfib_app [lemma, in Fib]
sumfib_eqn' [lemma, in Fib]
sumfib_eqn [lemma, in Fib]
sumfib_cons [lemma, in Fib]
S_evens [lemma, in Fib]
T
tau [definition, in Phi]tau_irr [lemma, in Phi]
tau_bound [lemma, in Phi]
tau_inv [lemma, in Phi]
tau_nz [lemma, in Phi]
tau_tau [lemma, in Phi]
tau_phi [lemma, in Phi]
tau_1 [lemma, in Phi]
Three [definition, in Fib]
ThreeEven [definition, in Fib]
ThreeEven_alt [lemma, in Fib]
ThreeEven_not_ThreeOdd' [lemma, in Fib]
ThreeEven_12 [lemma, in Fib]
ThreeEven_21 [lemma, in Fib]
ThreeEven_not_ThreeOdd [lemma, in Fib]
ThreeEven_Three [lemma, in Fib]
ThreeEven_le [lemma, in Fib]
ThreeEven_Sg [lemma, in FunG]
ThreeOdd [definition, in Fib]
ThreeOdd_next_inv [lemma, in Fib]
ThreeOdd_next8 [lemma, in Fib]
ThreeOdd_next5 [lemma, in Fib]
ThreeOdd_next_5_xor_8 [lemma, in Fib]
ThreeOdd_add_7 [lemma, in Fib]
ThreeOdd_add_6 [lemma, in Fib]
ThreeOdd_add_4 [lemma, in Fib]
ThreeOdd_add_3 [lemma, in Fib]
ThreeOdd_add_2 [lemma, in Fib]
ThreeOdd_add_1 [lemma, in Fib]
ThreeOdd_next [lemma, in Fib]
ThreeOdd_alt [lemma, in Fib]
ThreeOdd_12 [lemma, in Fib]
ThreeOdd_Three [lemma, in Fib]
ThreeOdd_le [lemma, in Fib]
ThreeOdd_Sg [lemma, in FunG]
Three_pred_Two [lemma, in Fib]
Three_succ_EvenHigh [lemma, in Fib]
Three_succ_Four [lemma, in Fib]
Three_Odd [lemma, in Fib]
Three_split [lemma, in Fib]
Three_12 [lemma, in Fib]
Three_21 [lemma, in Fib]
Three_g [lemma, in FunG]
Two [definition, in Fib]
Two_pred_High [lemma, in Fib]
Two_succ_Odd [lemma, in Fib]
Two_succ_Three [lemma, in Fib]
Two_Even [lemma, in Fib]
Two_not_ThreeOdd' [lemma, in Fib]
Two_not_ThreeOdd [lemma, in Fib]
Two_not_Three'' [lemma, in Fib]
Two_not_Three' [lemma, in Fib]
Two_not_Three [lemma, in Fib]
Two_not_High [lemma, in Fib]
Two_12 [lemma, in Fib]
Two_21 [lemma, in Fib]
Two_g [lemma, in FunG]
U
Unary [definition, in FunG]unary_child_is_binary [lemma, in FlipG]
unary_xor_multary [lemma, in FlipG]
unary_or_multary [lemma, in FlipG]
unary_flip [lemma, in FlipG]
unary_rchild_is_binary [lemma, in FunG]
unary_xor_multary [lemma, in FunG]
unary_or_multary [lemma, in FunG]
unary_carac2 [lemma, in FunG]
unary_carac1 [lemma, in FunG]
other
_ ^^ _ [notation, in FunG]Notation Index
other
_ ^^ _ [in FunG]Library Index
D
DeltaListF
FibFlipG
FunG
FunG_prog
P
PhiLemma Index
A
alt_mono_is_fg [in FlipG]alt_mono_unique [in FlipG]
alt_mono_bound [in FlipG]
alt_5 [in FlipG]
alt_4 [in FlipG]
alt_bound' [in FlipG]
alt_bound [in FlipG]
alt_spec_oups [in FlipG]
alt_spec_fg [in FlipG]
B
binary_rchild_is_binary [in FlipG]binary_lchild_is_unary [in FlipG]
binary_rchild_is_unary [in FunG]
binary_lchild_is_binary [in FunG]
binary_carac2 [in FunG]
binary_carac1 [in FunG]
D
decomp_complete' [in Fib]decomp_complete [in Fib]
decomp_unique [in Fib]
decomp_exists [in Fib]
decomp_unique_rev [in Fib]
decomp_exists_rev [in Fib]
decomp_max [in Fib]
decomp_binary_iff [in FunG]
decomp_unary_iff [in FunG]
decomp_binary [in FunG]
decomp_unary [in FunG]
decomp_rchild [in FunG]
DeltaRev_rev [in DeltaList]
DeltaRev_app_inv [in DeltaList]
DeltaRev_app [in DeltaList]
DeltaRev_alt [in DeltaList]
delta_eqn [in FlipG]
delta_bc [in FlipG]
delta_c [in FlipG]
delta_b [in FlipG]
delta_a [in FlipG]
delta_0_1 [in FlipG]
Delta_rev [in DeltaList]
Delta_app_inv [in DeltaList]
Delta_app [in DeltaList]
Delta_seq [in DeltaList]
Delta_pred [in DeltaList]
Delta_map [in DeltaList]
Delta_21_S [in DeltaList]
Delta_low_hd [in DeltaList]
Delta_nz [in DeltaList]
Delta_21 [in DeltaList]
Delta_more [in DeltaList]
Delta_inv [in DeltaList]
Delta_alt [in DeltaList]
Delta_odds [in Fib]
Delta_evens [in Fib]
delta_eqn [in FunG]
delta_b [in FunG]
delta_a [in FunG]
delta_0_1 [in FunG]
depth_carac [in FunG]
depth_0 [in FunG]
depth_Sfib [in FunG]
depth_fib [in FunG]
depth_mono [in FunG]
depth_minimal [in FunG]
depth_correct [in FunG]
depth_eqn [in FunG]
depth_SS [in FunG]
E
EvenHigh_pred_ThreeOdd [in Fib]EvenHigh_pred_Odd [in Fib]
evens_in [in Fib]
evens_S [in Fib]
Even_not_ThreeOdd [in Fib]
Even_12 [in Fib]
Even_xor_Odd [in Fib]
Even_or_Odd [in Fib]
Even_gP [in FunG]
Even_g [in FunG]
F
FD_step [in FlipG]FD_unique [in FlipG]
FD_lt [in FlipG]
FD_nz [in FlipG]
FD_le [in FlipG]
fg_alt_eqn [in FlipG]
fg_c_inv [in FlipG]
fg_c [in FlipG]
fg_b [in FlipG]
fg_a [in FlipG]
fg_unique [in FlipG]
fg_implements_FD [in FlipG]
fg_g_step [in FlipG]
fg_g [in FlipG]
fg_g_aux3 [in FlipG]
fg_g_aux2 [in FlipG]
fg_g_aux1 [in FlipG]
fg_g_aux0 [in FlipG]
fg_g_eq_inv [in FlipG]
fg_g_S_inv [in FlipG]
fg_children [in FlipG]
fg_onto_eqn' [in FlipG]
fg_onto_eqn [in FlipG]
fg_multary_binary [in FlipG]
fg_eqn_unique [in FlipG]
fg_eqn [in FlipG]
fg_inv [in FlipG]
fg_max_two_antecedents [in FlipG]
fg_nonflat [in FlipG]
fg_onto [in FlipG]
fg_lt [in FlipG]
fg_le [in FlipG]
fg_fix [in FlipG]
fg_nz [in FlipG]
fg_0_inv [in FlipG]
fg_nonzero [in FlipG]
fg_lipschitz [in FlipG]
fg_mono [in FlipG]
fg_mono_S [in FlipG]
fg_step [in FlipG]
fg_Sfib' [in FlipG]
fg_fib' [in FlipG]
fg_Sfib [in FlipG]
fg_fib [in FlipG]
fg_depth [in FlipG]
fib_inv [in Fib]
fib_le_id [in Fib]
fib_lt_inv [in Fib]
fib_inj [in Fib]
fib_mono [in Fib]
fib_mono_S [in Fib]
fib_lt [in Fib]
fib_lt_S [in Fib]
fib_0_inv [in Fib]
fib_nz [in Fib]
fib_S_nz [in Fib]
fib_eqn' [in Fib]
fib_eqn [in Fib]
flip_pred [in FlipG]
flip_S [in FlipG]
flip_high [in FlipG]
flip_low [in FlipG]
flip_swap [in FlipG]
flip_eq [in FlipG]
flip_flip [in FlipG]
flip_fib [in FlipG]
flip_Sfib [in FlipG]
flip_eqn [in FlipG]
flip_eqn0 [in FlipG]
flip_depth [in FlipG]
Four_pred_Three [in Fib]
G
GD_unique [in FunG]GS_inv [in FunG]
g_le_fg [in FlipG]
g_phi [in Phi]
g_tau [in Phi]
g_implements_GD [in FunG]
g_alt_def [in FunG]
g_pred_pred_fib [in FunG]
g_pred_fib_even [in FunG]
g_pred_fib_odd [in FunG]
g_not_Two [in FunG]
g_Two_iff [in FunG]
g_Two [in FunG]
g_Low' [in FunG]
g_Low [in FunG]
g_sumfib_rev [in FunG]
g_sumfib' [in FunG]
g_sumfib [in FunG]
g_depth [in FunG]
g_alt_eqn [in FunG]
g_lchild [in FunG]
g_children [in FunG]
g_Sfib' [in FunG]
g_Sfib [in FunG]
g_fib' [in FunG]
g_fib [in FunG]
g_onto_eqn [in FunG]
g_onto [in FunG]
g_inv [in FunG]
g_max_two_antecedents [in FunG]
g_div2_le [in FunG]
g_double_le [in FunG]
g_SS [in FunG]
g_nonflat' [in FunG]
g_nonflat [in FunG]
g_prev [in FunG]
g_next [in FunG]
g_lt [in FunG]
g_le [in FunG]
g_fix [in FunG]
g_nz [in FunG]
g_0_inv [in FunG]
g_nonzero [in FunG]
g_lipschitz [in FunG]
g_mono [in FunG]
g_mono_S [in FunG]
g_step [in FunG]
g_unique [in FunG]
g_S [in FunG]
g_eqn [in FunG]
g_0 [in FunG]
g_complete [in FunG]
g_correct [in FunG]
G_fun [in FunG]
G_rec [in FunG]
G_le [in FunG]
G1 [in FunG]
H
High_succ_Two [in Fib]High_not_ThreeOdd' [in Fib]
High_not_ThreeOdd [in Fib]
High_not_Three' [in Fib]
High_not_Three [in Fib]
High_12 [in Fib]
High_Sg [in FunG]
High_g [in FunG]
I
int_part_le [in Phi]int_frac [in Phi]
int_part_carac [in Phi]
int_part_iff [in Phi]
in_seq [in DeltaList]
iter_S [in FunG]
L
lchild_rchild [in FlipG]lchild_leftmost' [in FlipG]
lchild_leftmost [in FlipG]
lchild'_alt [in FlipG]
leftmost_son_is_binary [in FunG]
Low_le [in Fib]
Low_12 [in Fib]
Low_21 [in Fib]
Low_unique [in Fib]
Low_nz [in Fib]
Low_exists [in Fib]
M
map_S_pred [in FunG]map_ext_in [in FunG]
monotone_equiv [in FlipG]
multary_flip [in FlipG]
multary_binary [in FunG]
N
norm_le [in Fib]norm_hd [in Fib]
norm_ok' [in Fib]
norm_ok [in Fib]
norm_sum [in Fib]
norm_spec [in Fib]
nothing_new [in FunG_prog]
O
odds_in [in Fib]Odd_pred_Two [in Fib]
Odd_succ_Even [in Fib]
Odd_12 [in Fib]
Odd_gP [in FunG]
Odd_g [in FunG]
oups_alt_eqn [in FlipG]
oups_def [in FlipG]
P
phi_nz [in Phi]prime_irr [in Phi]
prime_5 [in Phi]
R
rchild_lchild [in FlipG]rightmost_son_is_binary [in FlipG]
rightmost_child_carac [in FlipG]
rightmost_child_carac [in FunG]
S
seq_end [in Fib]seq_S [in Fib]
sqrt5_irr [in Phi]
sumfib_odds [in Fib]
sumfib_evens [in Fib]
sumfib_0 [in Fib]
sumfib_rev [in Fib]
sumfib_app [in Fib]
sumfib_eqn' [in Fib]
sumfib_eqn [in Fib]
sumfib_cons [in Fib]
S_evens [in Fib]
T
tau_irr [in Phi]tau_bound [in Phi]
tau_inv [in Phi]
tau_nz [in Phi]
tau_tau [in Phi]
tau_phi [in Phi]
tau_1 [in Phi]
ThreeEven_alt [in Fib]
ThreeEven_not_ThreeOdd' [in Fib]
ThreeEven_12 [in Fib]
ThreeEven_21 [in Fib]
ThreeEven_not_ThreeOdd [in Fib]
ThreeEven_Three [in Fib]
ThreeEven_le [in Fib]
ThreeEven_Sg [in FunG]
ThreeOdd_next_inv [in Fib]
ThreeOdd_next8 [in Fib]
ThreeOdd_next5 [in Fib]
ThreeOdd_next_5_xor_8 [in Fib]
ThreeOdd_add_7 [in Fib]
ThreeOdd_add_6 [in Fib]
ThreeOdd_add_4 [in Fib]
ThreeOdd_add_3 [in Fib]
ThreeOdd_add_2 [in Fib]
ThreeOdd_add_1 [in Fib]
ThreeOdd_next [in Fib]
ThreeOdd_alt [in Fib]
ThreeOdd_12 [in Fib]
ThreeOdd_Three [in Fib]
ThreeOdd_le [in Fib]
ThreeOdd_Sg [in FunG]
Three_pred_Two [in Fib]
Three_succ_EvenHigh [in Fib]
Three_succ_Four [in Fib]
Three_Odd [in Fib]
Three_split [in Fib]
Three_12 [in Fib]
Three_21 [in Fib]
Three_g [in FunG]
Two_pred_High [in Fib]
Two_succ_Odd [in Fib]
Two_succ_Three [in Fib]
Two_Even [in Fib]
Two_not_ThreeOdd' [in Fib]
Two_not_ThreeOdd [in Fib]
Two_not_Three'' [in Fib]
Two_not_Three' [in Fib]
Two_not_Three [in Fib]
Two_not_High [in Fib]
Two_12 [in Fib]
Two_21 [in Fib]
Two_g [in FunG]
U
unary_child_is_binary [in FlipG]unary_xor_multary [in FlipG]
unary_or_multary [in FlipG]
unary_flip [in FlipG]
unary_rchild_is_binary [in FunG]
unary_xor_multary [in FunG]
unary_or_multary [in FunG]
unary_carac2 [in FunG]
unary_carac1 [in FunG]
Constructor Index
D
Dcons [in DeltaList]Dnil [in DeltaList]
Done [in DeltaList]
DRcons [in DeltaList]
DRnil [in DeltaList]
DRone [in DeltaList]
F
FD_c [in FlipG]FD_b [in FlipG]
FD_a [in FlipG]
FD_4 [in FlipG]
FD_3 [in FlipG]
FD_2 [in FlipG]
FD_1 [in FlipG]
FD_0 [in FlipG]
G
GD_b' [in FunG]GD_b [in FunG]
GD_a [in FunG]
GD_1 [in FunG]
GD_0 [in FunG]
GS [in FunG]
G0 [in FunG]
Inductive Index
D
Delta [in DeltaList]DeltaRev [in DeltaList]
F
FD [in FlipG]G
G [in FunG]GD [in FunG]
Definition Index
A
AltSpec [in FlipG]B
Binary [in FunG]D
d [in FlipG]d [in FunG]
depth [in FunG]
E
Even [in Fib]evens [in Fib]
F
fg [in FlipG]fib [in Fib]
flip [in FlipG]
Four [in Fib]
G
g [in FunG_prog]g [in FunG]
g_spec [in FunG_prog]
g_spec [in FunG]
H
HeadLeEven [in Fib]High [in Fib]
I
IHeq [in FlipG]IHsucc [in FlipG]
L
lchild [in FlipG]lchild [in FunG]
Low [in Fib]
M
Multary [in FunG]N
norm [in Fib]O
Odd [in Fib]odds [in Fib]
oups [in FlipG]
P
phi [in Phi]R
rchild [in FlipG]rchild [in FunG]
S
sumfib [in Fib]T
tau [in Phi]Three [in Fib]
ThreeEven [in Fib]
ThreeOdd [in Fib]
Two [in Fib]
U
Unary [in FunG]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (398 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (328 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
This page has been generated by coqdoc