Formalisation of GMP Square Root
Dependency Graph
| 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 |
_ |
(390 entries) |
| Tactic 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 |
_ |
(6 entries) |
| Axiom 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 |
_ |
(3 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 |
_ |
(277 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 |
_ |
(3 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 |
_ |
(3 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 |
_ |
(54 entries) |
| Module 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 |
_ |
(44 entries) |
Global Index
A
add_pos_le [lemma, in sqrt_prog]
add_un_add [lemma, in nat_morphism2]
add_un_add [lemma, in nat_morphism]
already_normalized_ok [lemma, in top_sqrt]
auxiliary_for_sqrt_goals1 [lemma, in sqrt_goals2]
aux_shift_1 [definition, in specifications]
aux_1 [lemma, in sqrt_prog]
aux_10 [lemma, in sqrt_prog]
aux_11 [lemma, in sqrt_prog]
aux_12 [lemma, in sqrt_prog]
aux_13 [lemma, in sqrt_prog]
aux_2 [lemma, in sqrt_prog]
aux_3 [lemma, in sqrt_prog]
aux_4 [lemma, in sqrt_prog]
aux_5 [lemma, in sqrt_prog]
aux_6 [lemma, in sqrt_prog]
aux_7 [lemma, in sqrt_prog]
aux_8 [lemma, in sqrt_prog]
aux_9 [lemma, in sqrt_prog]
A1 [lemma, in Zextensions]
A1' [lemma, in lemmas]
A2 [lemma, in Zextensions]
B
b [definition, in fun]
b [definition, in top_sqrt]
beta [definition, in top_sqrt]
beta [definition, in specifications]
betaGt0 [lemma, in mpn_complements]
betaGt0 [lemma, in top_sqrt]
betaGt1 [axiom, in specifications]
betaGt2 [lemma, in mpn_complements]
betaMultipleTwo [lemma, in top_sqrt]
beta' [axiom, in specifications]
between_0_1 [lemma, in sqrt_prog]
between_0_1' [lemma, in sqrt_prog]
bool2nat [definition, in sqrt_prog]
bool2Z [definition, in sqrt_prog]
borrow_bound [lemma, in mpn_complements]
borrow_positive [lemma, in mpn_complements]
borrow_positive' [lemma, in mpn_complements]
bound [axiom, in specifications]
bPos [lemma, in fun]
bPowPos [lemma, in fun]
build_aux_thms [module]
C
c [definition, in top_sqrt]
ceildivPos [lemma, in div2]
ceildiv2 [definition, in div2]
ceildiv2' [definition, in div2]
ceildiv2_aux_lemma [lemma, in div2]
ceildiv2_characteristic [lemma, in div2]
ceildiv2_eq [lemma, in div2]
compute_POS [tactic definition, in compute_POS]
compute_POS [module]
correct_goals [module]
correct_goal1 [lemma, in correct_goals]
correct_goal2 [lemma, in correct_goals]
correct_goal3 [lemma, in correct_goals]
correct_goal4 [lemma, in correct_goals]
correct_goal5 [lemma, in correct_goals]
correct_goal6 [lemma, in correct_goals]
correct_goal7 [lemma, in correct_goals]
correct_result [module]
c_decompose [constructor, in fun_aux]
c_sqrt [constructor, in sqrtrembase]
D
decompose [definition, in fun_aux]
divDefBreakdown2 [tactic definition, in proof_sqrt]
divDefBreakdown3 [tactic definition, in proof_sqrt]
divDefBreakdown4 [tactic definition, in proof_sqrt]
division_step [module]
divltle2 [lemma, in top_misc]
divrem' [definition, in fun]
div2 [module]
div2' [definition, in sqrt_prog]
div2_double_le [lemma, in sqrt_prog]
div2_floordiv2_equal [lemma, in sqrt_prog]
div2_le [lemma, in sqrt_prog]
div2_minus [lemma, in sqrt_prog]
div2_minus' [lemma, in sqrt_prog]
div2_minus_lt [lemma, in sqrt_prog]
div2_mult2 [lemma, in sqrt_prog]
div2_nn_l [lemma, in sqrt_prog]
div2_odd [lemma, in sqrt_prog]
div2_thm1 [lemma, in top_misc]
div2_thm2 [lemma, in top_misc]
div2_thm3 [lemma, in top_misc]
div2_thm4 [lemma, in top_misc]
div2_01 [lemma, in top_misc]
div_goals [module]
div_goals10 [module]
div_goals11 [module]
div_goals12 [module]
div_goals13 [module]
div_goals2 [module]
div_goals3 [module]
div_goals4 [module]
div_goals5 [module]
div_goals6 [module]
div_goals7 [module]
div_goals8 [module]
div_goals9 [module]
div_goal1 [lemma, in div_goals]
div_goal10 [lemma, in div_goals10]
div_goal11 [lemma, in div_goals11]
div_goal12 [lemma, in div_goals12]
div_goal13 [lemma, in div_goals13]
div_goal2 [lemma, in div_goals2]
div_goal3 [lemma, in div_goals3]
div_goal4 [lemma, in div_goals4]
div_goal5 [lemma, in div_goals5]
div_goal6 [lemma, in div_goals6]
div_goal7 [lemma, in div_goals7]
div_goal8 [lemma, in div_goals8]
div_goal9 [lemma, in div_goals9]
div_rem_uniqueness [lemma, in top_sqrt]
E
easy_thm1 [lemma, in top_sqrt]
easy_thm2 [lemma, in top_sqrt]
exponentbMulipleFour [lemma, in fun_aux]
exponentbMulipleFour [lemma, in fun]
F
floordiv2 [definition, in div2]
floordiv2_ge [lemma, in div2]
floordiv2_le_ceildiv2 [lemma, in div2]
former_prop4 [lemma, in proof_sqrt]
fun [module]
fun_aux [module]
f' [definition, in specifications]
G
Gomega [module]
H
hdiv_decrease [lemma, in div2]
Hhalfpos [lemma, in proof_sqrt]
Hhalf_easy [lemma, in sqrt_prog]
Hpos [lemma, in proof_sqrt]
I
I [definition, in specifications]
implies_normalized [lemma, in top_sqrt]
implies_normalized_N1 [lemma, in top_sqrt]
Impnumber_access [lemma, in mpn_complements]
Impnumber_between [lemma, in mpn_complements]
Impnumber_bound [lemma, in mpn_complements]
Impnumber_decompose [lemma, in mpn_complements]
Impnumber_unchanged [lemma, in mpn_complements]
Impnumber_unchanged_bis [lemma, in mpn_complements]
inj_minus_div2 [lemma, in sqrt_prog]
isEvenOrOdd [definition, in specifications]
IsNormalized [definition, in proof_sqrt]
I_decompose_divprop [lemma, in sqrt_prog]
I_positive [lemma, in mpn_complements]
K
k [definition, in top_sqrt]
L
lemmas [module]
length_n_decompose [lemma, in memory]
le_ceildiv2' [lemma, in div2]
le_ceildiv2' [lemma, in fun_aux]
le_div2_minus [lemma, in sqrt_prog]
le_Zle [lemma, in nat_morphism2]
le_Zle [lemma, in nat_morphism]
lt1_le0 [lemma, in sqrt_prog]
lt_ceildiv2' [lemma, in fun_aux]
lt_ceildiv2' [lemma, in div2]
lt_floordiv [lemma, in fun_aux]
lt_floordiv [lemma, in div2]
lt_minus_div2 [lemma, in sqrt_prog]
lt_O_div2 [lemma, in sqrt_prog]
L1 [lemma, in proof_sqrt]
l1 [lemma, in lemmas]
l10 [lemma, in lemmas]
l11 [lemma, in lemmas]
l12 [lemma, in lemmas]
l14 [lemma, in lemmas]
l15 [lemma, in lemmas]
l16 [lemma, in lemmas]
l17 [lemma, in lemmas]
l2 [lemma, in lemmas]
L2 [lemma, in proof_sqrt]
L3 [lemma, in proof_sqrt]
l3 [lemma, in lemmas]
l4 [lemma, in lemmas]
L4 [lemma, in Zextensions]
L4' [lemma, in Zextensions]
L5 [lemma, in Zextensions]
l5 [lemma, in lemmas]
L6 [lemma, in Zextensions]
l6 [lemma, in lemmas]
l7 [lemma, in lemmas]
L7 [lemma, in Zextensions]
l8 [lemma, in lemmas]
l9 [lemma, in lemmas]
M
memory [module]
minus_div2_S [lemma, in sqrt_prog]
modZ [definition, in specifications]
modZtoZ [definition, in specifications]
modZ_xH [lemma, in specifications]
modZ_ZERO [lemma, in specifications]
mpn_complements [module]
mult_morphism [lemma, in nat_morphism]
mult_morphism [lemma, in nat_morphism2]
m1_m [lemma, in memory]
m2_m [lemma, in memory]
m2_m' [lemma, in memory]
N
nat_half_decompose [inductive, in fun_aux]
nat_morphism [module]
nat_morphism2 [module]
nn_even_implies_2tn_is_nn [lemma, in top_sqrt]
nn_odd_implies_2tn_is_nn [lemma, in top_sqrt]
normalization_propagation [lemma, in proof_sqrt]
normalized_base_case [lemma, in fun]
normalized_base_case_aux [lemma, in fun]
normalized_divide [lemma, in fun_aux]
normalized_div2 [lemma, in fun_aux]
normalized_positive [lemma, in fun]
normalized_positive_l [lemma, in proof_sqrt]
no_overlap [definition, in specifications]
Npos [lemma, in proof_sqrt]
Ntstrictpos [lemma, in top_sqrt]
Ntsup [lemma, in top_sqrt]
Nts0 [lemma, in top_sqrt]
N''pos [lemma, in proof_sqrt]
N0ltL [lemma, in proof_sqrt]
N0pos [lemma, in proof_sqrt]
N1ltL [lemma, in proof_sqrt]
N1_22k_Nt [lemma, in top_sqrt]
O
Omega' [tactic definition, in tacdef]
one_le_minus_div2 [lemma, in sqrt_prog]
others_are_unchanged [lemma, in memory]
P
plus_morphism [lemma, in nat_morphism]
plus_morphism [lemma, in nat_morphism2]
Post_mpn_addmul_1 [definition, in specifications]
pow [definition, in pow]
pow [module]
powbetaGt0 [lemma, in top_sqrt]
pow_beta_b [lemma, in top_sqrt]
pow_b_is_even [lemma, in fun]
pow_ceil_ge_pow_floor [lemma, in div2]
pow_decompose [lemma, in div2]
pow_div2 [lemma, in sqrt_prog]
pow_h_ge_pow_l [lemma, in sqrt_prog]
pow_monotonous [lemma, in pow]
pow_morphism [lemma, in nat_morphism2]
pow_morphism [lemma, in nat_morphism]
pow_mult [lemma, in pow]
pow_nat [definition, in nat_morphism]
pow_nat [definition, in nat_morphism2]
pow_pos [lemma, in pow]
pow_positive [lemma, in mpn_complements]
pow_positive' [lemma, in sqrt_prog]
pow_sum [lemma, in pow]
proof_sqrt [module]
Q
Qge1 [lemma, in proof_sqrt]
QleL [lemma, in proof_sqrt]
Qpos [lemma, in proof_sqrt]
quotype [inductive, in fun_aux]
quo_type_def [constructor, in fun_aux]
q0pos [lemma, in top_sqrt]
R
R'pos [lemma, in proof_sqrt]
R''pos [lemma, in proof_sqrt]
R1 [definition, in proof_sqrt]
R2 [definition, in fun_aux]
R2_eq1 [lemma, in fun_aux]
R2_eq2 [lemma, in fun_aux]
S
Sfinal [lemma, in proof_sqrt]
shift_2 [definition, in specifications]
SolveBounds [tactic definition, in tacdef]
specifications [module]
sqrtrem [definition, in fun]
sqrtrembase [definition, in fun]
sqrtrembase [module]
sqrtrempos [definition, in sqrtrembase]
SqrtremProp [definition, in proof_sqrt]
SqrtremProp1 [definition, in proof_sqrt]
SqrtremProp2 [definition, in proof_sqrt]
SqrtremProp3 [definition, in proof_sqrt]
SqrtremProp4 [definition, in proof_sqrt]
sqrt_data [inductive, in sqrtrembase]
sqrt_F [definition, in fun]
sqrt_F_type [definition, in fun]
sqrt_goals [module]
sqrt_goals2 [module]
sqrt_goals3 [module]
sqrt_goals4 [module]
sqrt_goals9_1' [lemma, in build_aux_thms]
sqrt_goals9_2' [lemma, in build_aux_thms]
sqrt_goals9_3' [lemma, in build_aux_thms]
sqrt_goals9_4' [lemma, in build_aux_thms]
sqrt_goals9_5' [lemma, in build_aux_thms]
sqrt_goals9_6' [lemma, in build_aux_thms]
sqrt_goals9_7' [lemma, in build_aux_thms]
sqrt_goal1 [lemma, in sqrt_goals]
sqrt_goal10 [lemma, in sqrt_goals4]
sqrt_goal2 [lemma, in sqrt_goals]
sqrt_goal3 [lemma, in sqrt_goals]
sqrt_goal4 [lemma, in sqrt_goals]
sqrt_goal5 [lemma, in sqrt_goals]
sqrt_goal6 [lemma, in sqrt_goals2]
sqrt_goal7 [lemma, in sqrt_goals2]
sqrt_goal8 [lemma, in sqrt_goals2]
sqrt_goal9 [lemma, in sqrt_goals3]
sqrt_prog [module]
sqrt_prog1 [module]
square_monotone [lemma, in sqrt_prog]
square_positive [lemma, in sqrt_prog]
square_pow [lemma, in pow]
sub_goals [module]
sub_goals2 [module]
sub_goal1 [lemma, in sub_goals]
sub_goal2 [lemma, in sub_goals]
sub_goal3 [lemma, in sub_goals]
sub_goal4 [lemma, in sub_goals]
sub_goal5 [lemma, in sub_goals2]
sub_square [module]
suppress_1 [lemma, in lemmas]
s0pos [lemma, in top_sqrt]
S1 [definition, in proof_sqrt]
S1pos [lemma, in top_sqrt]
S2 [definition, in fun_aux]
S2pos [lemma, in proof_sqrt]
S2_eq1 [lemma, in fun_aux]
S2_eq2 [lemma, in fun_aux]
S3 [lemma, in proof_sqrt]
S4 [lemma, in proof_sqrt]
S_morphism [lemma, in nat_morphism2]
S_morphism [lemma, in nat_morphism]
T
tacdef [module]
thm_between [lemma, in top_sqrt]
thm_between' [lemma, in top_sqrt]
thm_between_Nt [lemma, in top_sqrt]
thm_final [lemma, in top_sqrt]
thm_Qdiv2q0 [lemma, in top_sqrt]
thm_q0s0 [lemma, in top_sqrt]
thm_R [lemma, in top_sqrt]
thm_R2 [lemma, in top_sqrt]
thm_R3 [lemma, in top_sqrt]
thm_R3' [lemma, in top_sqrt]
thm_R3'' [lemma, in top_sqrt]
thm_topsqrtremprop1 [lemma, in top_sqrt]
thm_Zsquare [lemma, in pow]
thm_Zsquare2 [lemma, in pow]
tn [definition, in top_sqrt]
top_misc [module]
top_sqrt [module]
two_step_ind [lemma, in sqrt_prog]
two_step_ind [lemma, in div2]
two_2 [lemma, in sqrt_prog]
T1 [lemma, in proof_sqrt]
T1_aux [lemma, in proof_sqrt]
U
using_Ntsup [lemma, in top_sqrt]
V
v12 [lemma, in lemmas]
Z
Zdivprop' [definition, in proof_sqrt]
Zdivprop1' [definition, in proof_sqrt]
Zdivprop2' [definition, in proof_sqrt]
Zdivprop3' [definition, in proof_sqrt]
Zdivprop4' [definition, in proof_sqrt]
Zextensions [module]
Zgt_not_le' [lemma, in Zextensions]
Zgt_S_le' [lemma, in Zextensions]
Zle_lt_1 [lemma, in Zextensions]
Zle_mult' [lemma, in Zextensions]
Zle_mult_simpl' [lemma, in Zextensions]
Zle_mult_2 [lemma, in mpn_complements]
Zle_Zmult_right' [lemma, in Zextensions]
Zle_Zmult_right2' [lemma, in Zextensions]
Zlt_left_plus [lemma, in Zextensions]
Zlt_mult_l [lemma, in sqrt_prog]
Zlt_mult_r [lemma, in sqrt_prog]
zlt_zero_beta [lemma, in sqrt_goals]
Zlt_Zmult_left [lemma, in Zextensions]
Zlt_Zmult_right [lemma, in Zextensions]
Zlt_Zmult_right2' [lemma, in Zextensions]
Zminus [definition, in correct_result]
Zminus_minus_assoc [lemma, in sqrt_prog]
Zminus_permute [lemma, in sqrt_prog]
Zminus_permute_square [lemma, in sqrt_prog]
Zminus_plus_assoc [lemma, in sqrt_prog]
Zminus_plus_permute [lemma, in sqrt_prog]
Zminus_plus_permute_square [lemma, in sqrt_prog]
Zminus_Zsquare [lemma, in pow]
Zmod [definition, in fun]
Zmultbool [definition, in specifications]
Zmultbool_to_Zmult [lemma, in sqrt_prog]
Zmult_le' [lemma, in Zextensions]
Zmult_lt' [lemma, in Zextensions]
Zmult_reg_left' [lemma, in Zextensions]
Zmult_reg_r [lemma, in lemmas]
Zmult_Zsquare [lemma, in pow]
Zplus_minus2 [lemma, in sqrt_prog]
Zplus_minus_assoc [lemma, in sqrt_prog]
Zplus_Zsquare [lemma, in pow]
Zquo [definition, in fun]
Zsquare [definition, in pow]
Zsquare_monotonous [lemma, in pow]
Zsquare_order [lemma, in pow]
Z0lt_le_pred [lemma, in Zextensions]
Z2bool [definition, in sqrt_prog]
Z_le_lt_dec [lemma, in Zextensions]
Z_lt_le_bool [definition, in correct_result]
Z_lt_le_dec [lemma, in Zextensions]
Tactic Index
C
compute_POS [in compute_POS]
D
divDefBreakdown2 [in proof_sqrt]
divDefBreakdown3 [in proof_sqrt]
divDefBreakdown4 [in proof_sqrt]
O
Omega' [in tacdef]
S
SolveBounds [in tacdef]
Axiom Index
B
betaGt1 [in specifications]
beta' [in specifications]
bound [in specifications]
Lemma Index
A
add_pos_le [in sqrt_prog]
add_un_add [in nat_morphism2]
add_un_add [in nat_morphism]
already_normalized_ok [in top_sqrt]
auxiliary_for_sqrt_goals1 [in sqrt_goals2]
aux_1 [in sqrt_prog]
aux_10 [in sqrt_prog]
aux_11 [in sqrt_prog]
aux_12 [in sqrt_prog]
aux_13 [in sqrt_prog]
aux_2 [in sqrt_prog]
aux_3 [in sqrt_prog]
aux_4 [in sqrt_prog]
aux_5 [in sqrt_prog]
aux_6 [in sqrt_prog]
aux_7 [in sqrt_prog]
aux_8 [in sqrt_prog]
aux_9 [in sqrt_prog]
A1 [in Zextensions]
A1' [in lemmas]
A2 [in Zextensions]
B
betaGt0 [in mpn_complements]
betaGt0 [in top_sqrt]
betaGt2 [in mpn_complements]
betaMultipleTwo [in top_sqrt]
between_0_1 [in sqrt_prog]
between_0_1' [in sqrt_prog]
borrow_bound [in mpn_complements]
borrow_positive [in mpn_complements]
borrow_positive' [in mpn_complements]
bPos [in fun]
bPowPos [in fun]
C
ceildivPos [in div2]
ceildiv2_aux_lemma [in div2]
ceildiv2_characteristic [in div2]
ceildiv2_eq [in div2]
correct_goal1 [in correct_goals]
correct_goal2 [in correct_goals]
correct_goal3 [in correct_goals]
correct_goal4 [in correct_goals]
correct_goal5 [in correct_goals]
correct_goal6 [in correct_goals]
correct_goal7 [in correct_goals]
D
divltle2 [in top_misc]
div2_double_le [in sqrt_prog]
div2_floordiv2_equal [in sqrt_prog]
div2_le [in sqrt_prog]
div2_minus [in sqrt_prog]
div2_minus' [in sqrt_prog]
div2_minus_lt [in sqrt_prog]
div2_mult2 [in sqrt_prog]
div2_nn_l [in sqrt_prog]
div2_odd [in sqrt_prog]
div2_thm1 [in top_misc]
div2_thm2 [in top_misc]
div2_thm3 [in top_misc]
div2_thm4 [in top_misc]
div2_01 [in top_misc]
div_goal1 [in div_goals]
div_goal10 [in div_goals10]
div_goal11 [in div_goals11]
div_goal12 [in div_goals12]
div_goal13 [in div_goals13]
div_goal2 [in div_goals2]
div_goal3 [in div_goals3]
div_goal4 [in div_goals4]
div_goal5 [in div_goals5]
div_goal6 [in div_goals6]
div_goal7 [in div_goals7]
div_goal8 [in div_goals8]
div_goal9 [in div_goals9]
div_rem_uniqueness [in top_sqrt]
E
easy_thm1 [in top_sqrt]
easy_thm2 [in top_sqrt]
exponentbMulipleFour [in fun_aux]
exponentbMulipleFour [in fun]
F
floordiv2_ge [in div2]
floordiv2_le_ceildiv2 [in div2]
former_prop4 [in proof_sqrt]
H
hdiv_decrease [in div2]
Hhalfpos [in proof_sqrt]
Hhalf_easy [in sqrt_prog]
Hpos [in proof_sqrt]
I
implies_normalized [in top_sqrt]
implies_normalized_N1 [in top_sqrt]
Impnumber_access [in mpn_complements]
Impnumber_between [in mpn_complements]
Impnumber_bound [in mpn_complements]
Impnumber_decompose [in mpn_complements]
Impnumber_unchanged [in mpn_complements]
Impnumber_unchanged_bis [in mpn_complements]
inj_minus_div2 [in sqrt_prog]
I_decompose_divprop [in sqrt_prog]
I_positive [in mpn_complements]
L
length_n_decompose [in memory]
le_ceildiv2' [in div2]
le_ceildiv2' [in fun_aux]
le_div2_minus [in sqrt_prog]
le_Zle [in nat_morphism2]
le_Zle [in nat_morphism]
lt1_le0 [in sqrt_prog]
lt_ceildiv2' [in fun_aux]
lt_ceildiv2' [in div2]
lt_floordiv [in fun_aux]
lt_floordiv [in div2]
lt_minus_div2 [in sqrt_prog]
lt_O_div2 [in sqrt_prog]
L1 [in proof_sqrt]
l1 [in lemmas]
l10 [in lemmas]
l11 [in lemmas]
l12 [in lemmas]
l14 [in lemmas]
l15 [in lemmas]
l16 [in lemmas]
l17 [in lemmas]
l2 [in lemmas]
L2 [in proof_sqrt]
L3 [in proof_sqrt]
l3 [in lemmas]
l4 [in lemmas]
L4 [in Zextensions]
L4' [in Zextensions]
L5 [in Zextensions]
l5 [in lemmas]
L6 [in Zextensions]
l6 [in lemmas]
l7 [in lemmas]
L7 [in Zextensions]
l8 [in lemmas]
l9 [in lemmas]
M
minus_div2_S [in sqrt_prog]
modZ_xH [in specifications]
modZ_ZERO [in specifications]
mult_morphism [in nat_morphism]
mult_morphism [in nat_morphism2]
m1_m [in memory]
m2_m [in memory]
m2_m' [in memory]
N
nn_even_implies_2tn_is_nn [in top_sqrt]
nn_odd_implies_2tn_is_nn [in top_sqrt]
normalization_propagation [in proof_sqrt]
normalized_base_case [in fun]
normalized_base_case_aux [in fun]
normalized_divide [in fun_aux]
normalized_div2 [in fun_aux]
normalized_positive [in fun]
normalized_positive_l [in proof_sqrt]
Npos [in proof_sqrt]
Ntstrictpos [in top_sqrt]
Ntsup [in top_sqrt]
Nts0 [in top_sqrt]
N''pos [in proof_sqrt]
N0ltL [in proof_sqrt]
N0pos [in proof_sqrt]
N1ltL [in proof_sqrt]
N1_22k_Nt [in top_sqrt]
O
one_le_minus_div2 [in sqrt_prog]
others_are_unchanged [in memory]
P
plus_morphism [in nat_morphism]
plus_morphism [in nat_morphism2]
powbetaGt0 [in top_sqrt]
pow_beta_b [in top_sqrt]
pow_b_is_even [in fun]
pow_ceil_ge_pow_floor [in div2]
pow_decompose [in div2]
pow_div2 [in sqrt_prog]
pow_h_ge_pow_l [in sqrt_prog]
pow_monotonous [in pow]
pow_morphism [in nat_morphism2]
pow_morphism [in nat_morphism]
pow_mult [in pow]
pow_pos [in pow]
pow_positive [in mpn_complements]
pow_positive' [in sqrt_prog]
pow_sum [in pow]
Q
Qge1 [in proof_sqrt]
QleL [in proof_sqrt]
Qpos [in proof_sqrt]
q0pos [in top_sqrt]
R
R'pos [in proof_sqrt]
R''pos [in proof_sqrt]
R2_eq1 [in fun_aux]
R2_eq2 [in fun_aux]
S
Sfinal [in proof_sqrt]
sqrt_goals9_1' [in build_aux_thms]
sqrt_goals9_2' [in build_aux_thms]
sqrt_goals9_3' [in build_aux_thms]
sqrt_goals9_4' [in build_aux_thms]
sqrt_goals9_5' [in build_aux_thms]
sqrt_goals9_6' [in build_aux_thms]
sqrt_goals9_7' [in build_aux_thms]
sqrt_goal1 [in sqrt_goals]
sqrt_goal10 [in sqrt_goals4]
sqrt_goal2 [in sqrt_goals]
sqrt_goal3 [in sqrt_goals]
sqrt_goal4 [in sqrt_goals]
sqrt_goal5 [in sqrt_goals]
sqrt_goal6 [in sqrt_goals2]
sqrt_goal7 [in sqrt_goals2]
sqrt_goal8 [in sqrt_goals2]
sqrt_goal9 [in sqrt_goals3]
square_monotone [in sqrt_prog]
square_positive [in sqrt_prog]
square_pow [in pow]
sub_goal1 [in sub_goals]
sub_goal2 [in sub_goals]
sub_goal3 [in sub_goals]
sub_goal4 [in sub_goals]
sub_goal5 [in sub_goals2]
suppress_1 [in lemmas]
s0pos [in top_sqrt]
S1pos [in top_sqrt]
S2pos [in proof_sqrt]
S2_eq1 [in fun_aux]
S2_eq2 [in fun_aux]
S3 [in proof_sqrt]
S4 [in proof_sqrt]
S_morphism [in nat_morphism2]
S_morphism [in nat_morphism]
T
thm_between [in top_sqrt]
thm_between' [in top_sqrt]
thm_between_Nt [in top_sqrt]
thm_final [in top_sqrt]
thm_Qdiv2q0 [in top_sqrt]
thm_q0s0 [in top_sqrt]
thm_R [in top_sqrt]
thm_R2 [in top_sqrt]
thm_R3 [in top_sqrt]
thm_R3' [in top_sqrt]
thm_R3'' [in top_sqrt]
thm_topsqrtremprop1 [in top_sqrt]
thm_Zsquare [in pow]
thm_Zsquare2 [in pow]
two_step_ind [in sqrt_prog]
two_step_ind [in div2]
two_2 [in sqrt_prog]
T1 [in proof_sqrt]
T1_aux [in proof_sqrt]
U
using_Ntsup [in top_sqrt]
V
v12 [in lemmas]
Z
Zgt_not_le' [in Zextensions]
Zgt_S_le' [in Zextensions]
Zle_lt_1 [in Zextensions]
Zle_mult' [in Zextensions]
Zle_mult_simpl' [in Zextensions]
Zle_mult_2 [in mpn_complements]
Zle_Zmult_right' [in Zextensions]
Zle_Zmult_right2' [in Zextensions]
Zlt_left_plus [in Zextensions]
Zlt_mult_l [in sqrt_prog]
Zlt_mult_r [in sqrt_prog]
zlt_zero_beta [in sqrt_goals]
Zlt_Zmult_left [in Zextensions]
Zlt_Zmult_right [in Zextensions]
Zlt_Zmult_right2' [in Zextensions]
Zminus_minus_assoc [in sqrt_prog]
Zminus_permute [in sqrt_prog]
Zminus_permute_square [in sqrt_prog]
Zminus_plus_assoc [in sqrt_prog]
Zminus_plus_permute [in sqrt_prog]
Zminus_plus_permute_square [in sqrt_prog]
Zminus_Zsquare [in pow]
Zmultbool_to_Zmult [in sqrt_prog]
Zmult_le' [in Zextensions]
Zmult_lt' [in Zextensions]
Zmult_reg_left' [in Zextensions]
Zmult_reg_r [in lemmas]
Zmult_Zsquare [in pow]
Zplus_minus2 [in sqrt_prog]
Zplus_minus_assoc [in sqrt_prog]
Zplus_Zsquare [in pow]
Zsquare_monotonous [in pow]
Zsquare_order [in pow]
Z0lt_le_pred [in Zextensions]
Z_le_lt_dec [in Zextensions]
Z_lt_le_dec [in Zextensions]
Constructor Index
C
c_decompose [in fun_aux]
c_sqrt [in sqrtrembase]
Q
quo_type_def [in fun_aux]
Inductive Index
N
nat_half_decompose [in fun_aux]
Q
quotype [in fun_aux]
S
sqrt_data [in sqrtrembase]
Definition Index
A
aux_shift_1 [in specifications]
B
b [in fun]
b [in top_sqrt]
beta [in top_sqrt]
beta [in specifications]
bool2nat [in sqrt_prog]
bool2Z [in sqrt_prog]
C
c [in top_sqrt]
ceildiv2 [in div2]
ceildiv2' [in div2]
D
decompose [in fun_aux]
divrem' [in fun]
div2' [in sqrt_prog]
F
floordiv2 [in div2]
f' [in specifications]
I
I [in specifications]
isEvenOrOdd [in specifications]
IsNormalized [in proof_sqrt]
K
k [in top_sqrt]
M
modZ [in specifications]
modZtoZ [in specifications]
N
no_overlap [in specifications]
P
Post_mpn_addmul_1 [in specifications]
pow [in pow]
pow_nat [in nat_morphism]
pow_nat [in nat_morphism2]
R
R1 [in proof_sqrt]
R2 [in fun_aux]
S
shift_2 [in specifications]
sqrtrem [in fun]
sqrtrembase [in fun]
sqrtrempos [in sqrtrembase]
SqrtremProp [in proof_sqrt]
SqrtremProp1 [in proof_sqrt]
SqrtremProp2 [in proof_sqrt]
SqrtremProp3 [in proof_sqrt]
SqrtremProp4 [in proof_sqrt]
sqrt_F [in fun]
sqrt_F_type [in fun]
S1 [in proof_sqrt]
S2 [in fun_aux]
T
tn [in top_sqrt]
Z
Zdivprop' [in proof_sqrt]
Zdivprop1' [in proof_sqrt]
Zdivprop2' [in proof_sqrt]
Zdivprop3' [in proof_sqrt]
Zdivprop4' [in proof_sqrt]
Zminus [in correct_result]
Zmod [in fun]
Zmultbool [in specifications]
Zquo [in fun]
Zsquare [in pow]
Z2bool [in sqrt_prog]
Z_lt_le_bool [in correct_result]
Module Index
B
build_aux_thms
C
compute_POS
correct_goals
correct_result
D
division_step
div2
div_goals
div_goals10
div_goals11
div_goals12
div_goals13
div_goals2
div_goals3
div_goals4
div_goals5
div_goals6
div_goals7
div_goals8
div_goals9
F
fun
fun_aux
G
Gomega
L
lemmas
M
memory
mpn_complements
N
nat_morphism
nat_morphism2
P
pow
proof_sqrt
S
specifications
sqrtrembase
sqrt_goals
sqrt_goals2
sqrt_goals3
sqrt_goals4
sqrt_prog
sqrt_prog1
sub_goals
sub_goals2
sub_square
T
tacdef
top_misc
top_sqrt
Z
Zextensions
| 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 |
_ |
(390 entries) |
| Tactic 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 |
_ |
(6 entries) |
| Axiom 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 |
_ |
(3 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 |
_ |
(277 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 |
_ |
(3 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 |
_ |
(3 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 |
_ |
(54 entries) |
| Module 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 |
_ |
(44 entries) |
This page has been generated by coqdoc