| 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 | (390 entries) |
| 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 | (17 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 | (217 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 | (74 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 | (19 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 | (63 entries) |
Global Index
A
ANd [constructor, in Presburger.Form]B
buildConj [definition, in Presburger.Form]buildConj_append [lemma, in Presburger.Form]
C
cnf [definition, in Presburger.Normal]Cnf [inductive, in Presburger.Normal]
CnfCnf1 [constructor, in Presburger.Normal]
CnfOr [constructor, in Presburger.Normal]
cnf_noBinder [lemma, in Presburger.Elim]
cnf_groundN [lemma, in Presburger.Normal]
cnf_correct [lemma, in Presburger.Normal]
cnf_cnf [lemma, in Presburger.Normal]
Cnf1 [inductive, in Presburger.Normal]
Cnf1And [constructor, in Presburger.Normal]
Cnf1Cnf2 [constructor, in Presburger.Normal]
Cnf1_cons [lemma, in Presburger.Normal]
Cnf1_app [lemma, in Presburger.Normal]
Cnf2 [inductive, in Presburger.Normal]
Cnf2Cong [constructor, in Presburger.Normal]
Cnf2Eq [constructor, in Presburger.Normal]
Cnf2False [constructor, in Presburger.Normal]
Cnf2NEq [constructor, in Presburger.Normal]
Cnf2True [constructor, in Presburger.Normal]
Cong [constructor, in Presburger.Form]
Cong [library]
congZ [definition, in Presburger.Cong]
congZ_O_Eq [lemma, in Presburger.Cong]
congZ_dec [definition, in Presburger.Cong]
congZ_mult [lemma, in Presburger.Cong]
congZ_minus [lemma, in Presburger.Cong]
congZ_plus [lemma, in Presburger.Cong]
congZ_trans [lemma, in Presburger.Cong]
congZ_sym [lemma, in Presburger.Cong]
congZ_id [lemma, in Presburger.Cong]
Contradict1 [lemma, in Presburger.sTactic]
Contradict2 [lemma, in Presburger.sTactic]
Contradict3 [lemma, in Presburger.sTactic]
correct_lift_quant [lemma, in Presburger.Lift]
correct_lift_neg [lemma, in Presburger.Lift]
correct_lift_andor_or [lemma, in Presburger.Lift]
correct_lift_andor_and [lemma, in Presburger.Lift]
correct_lift_if [lemma, in Presburger.Lift]
D
decideCorrect [lemma, in Presburger.Form]decideGround [definition, in Presburger.Form]
div [definition, in Presburger.Nat]
divides [definition, in Presburger.Nat]
divides_lcm3 [lemma, in Presburger.Nat]
divides_lcm2 [lemma, in Presburger.Nat]
divides_lcm1 [lemma, in Presburger.Nat]
divides_div [lemma, in Presburger.Nat]
divides_id [lemma, in Presburger.Nat]
divides_gcd3 [lemma, in Presburger.Nat]
divides_gcd1_aux [lemma, in Presburger.Nat]
divides_gcd2 [lemma, in Presburger.Nat]
divides_gcd1 [lemma, in Presburger.Nat]
divides_gcd_aux [lemma, in Presburger.Nat]
divides_minus [lemma, in Presburger.Nat]
divides_add [lemma, in Presburger.Nat]
divides_trans [lemma, in Presburger.Nat]
divides_refl [lemma, in Presburger.Nat]
div_lt_ZERO [lemma, in Presburger.Nat]
div_correct [lemma, in Presburger.Nat]
div1 [definition, in Presburger.Nat]
div1_correct [lemma, in Presburger.Nat]
E
econg [definition, in Presburger.Normal]econg_pneg [lemma, in Presburger.Normal]
econg_groundN [lemma, in Presburger.Normal]
econg_correct [lemma, in Presburger.Normal]
Elim [library]
elimQuant [definition, in Presburger.Elim]
elimQuants [definition, in Presburger.Elim]
elimQuants_groundN [lemma, in Presburger.Elim]
elimQuants_correct [lemma, in Presburger.Elim]
elimQuant_groundN [lemma, in Presburger.Elim]
elimQuant_correct [lemma, in Presburger.Elim]
Eq [constructor, in Presburger.Form]
Exists [constructor, in Presburger.Form]
exp [inductive, in Presburger.Form]
expand_forall_groundN [lemma, in Presburger.Normal]
expand_forall_correct [lemma, in Presburger.Normal]
expand_forall_normal [lemma, in Presburger.Normal]
expand_forall [definition, in Presburger.Normal]
expand_groundN [lemma, in Presburger.Normal]
expand_cong_correct [lemma, in Presburger.Normal]
expand_cong_pneg [lemma, in Presburger.Normal]
expand_cong [definition, in Presburger.Normal]
exp2Z [definition, in Presburger.Form]
exp2Z_ground [lemma, in Presburger.Form]
F
Factor [library]factorExp [definition, in Presburger.Factor]
factorExp_groundN [lemma, in Presburger.Factor]
factorExp_correct [lemma, in Presburger.Factor]
factorVar0 [definition, in Presburger.Factor]
factorVar0_groundN [lemma, in Presburger.Factor]
factorVar0_correct [lemma, in Presburger.Factor]
FAlse [constructor, in Presburger.Form]
fcong [definition, in Presburger.Cong]
fcong_correct [lemma, in Presburger.Cong]
fgroundNExp [definition, in Presburger.GroundN]
fgroundNForm [definition, in Presburger.GroundN]
fgrounNExp_correct [lemma, in Presburger.GroundN]
fgrounNForm_correct [lemma, in Presburger.GroundN]
Forall [constructor, in Presburger.Form]
form [inductive, in Presburger.Form]
Form [library]
formL2Prop [definition, in Presburger.Form]
formL2Prop_append [lemma, in Presburger.Form]
form2Prop [definition, in Presburger.Form]
form2Prop_app_inv [lemma, in Presburger.Form]
form2Prop_cons_inv [lemma, in Presburger.Form]
form2Prop_app [lemma, in Presburger.Form]
form2Prop_cons [lemma, in Presburger.Form]
G
GAnd [constructor, in Presburger.Form]gcd [definition, in Presburger.Nat]
gcd_lt_zero [lemma, in Presburger.Nat]
gcd_sym [lemma, in Presburger.Nat]
gcd_bezout [lemma, in Presburger.Nat]
gcd_O2 [lemma, in Presburger.Nat]
gcd_O1 [lemma, in Presburger.Nat]
gcd1 [definition, in Presburger.Nat]
gcd1_O [lemma, in Presburger.Nat]
gcd1_bezout [lemma, in Presburger.Nat]
gcd1_bezout1 [lemma, in Presburger.Nat]
gcd1_bezout0 [lemma, in Presburger.Nat]
GCong [constructor, in Presburger.Form]
GEq [constructor, in Presburger.Form]
GFalse [constructor, in Presburger.Form]
GImp [constructor, in Presburger.Form]
GNAnd [constructor, in Presburger.GroundN]
GNCong [constructor, in Presburger.GroundN]
GNeg [constructor, in Presburger.Form]
GNEq [constructor, in Presburger.GroundN]
GNExists [constructor, in Presburger.GroundN]
GNFalse [constructor, in Presburger.GroundN]
GNForall [constructor, in Presburger.GroundN]
GNImp [constructor, in Presburger.GroundN]
GNNeg [constructor, in Presburger.GroundN]
GNNil [constructor, in Presburger.GroundN]
GNNil2 [constructor, in Presburger.GroundN]
GNNum [constructor, in Presburger.GroundN]
GNOr [constructor, in Presburger.GroundN]
GNPlus [constructor, in Presburger.GroundN]
GNTrue [constructor, in Presburger.GroundN]
GNum [constructor, in Presburger.Form]
GNVar [constructor, in Presburger.GroundN]
GNVCons [constructor, in Presburger.GroundN]
GNVCons2 [constructor, in Presburger.GroundN]
GOr [constructor, in Presburger.Form]
GPlus [constructor, in Presburger.Form]
groundExp [inductive, in Presburger.Form]
groundForm [inductive, in Presburger.Form]
GroundN [library]
groundNExp [inductive, in Presburger.GroundN]
groundNExp_le [lemma, in Presburger.GroundN]
groundNForm [inductive, in Presburger.GroundN]
groundNForm_Cnf_groundForm_aux [lemma, in Presburger.Elim]
groundNForm_le [lemma, in Presburger.GroundN]
groundNL [inductive, in Presburger.GroundN]
groundNL_groundNForm [lemma, in Presburger.Elim]
groundNL_le [lemma, in Presburger.GroundN]
groundNL_app [lemma, in Presburger.GroundN]
groundNL2 [inductive, in Presburger.GroundN]
groundNL2_le [lemma, in Presburger.GroundN]
groundNL2_app [lemma, in Presburger.GroundN]
GTrue [constructor, in Presburger.Form]
I
Imp [constructor, in Presburger.Form]inj_oZ1 [lemma, in Presburger.Zdivides]
iso_lift_andor_or2 [lemma, in Presburger.Lift]
iso_lift_andor_and2 [lemma, in Presburger.Lift]
iso_lift_andor_or1 [lemma, in Presburger.Lift]
iso_lift_andor_and1 [lemma, in Presburger.Lift]
iso_lift_i2 [lemma, in Presburger.Lift]
iso_lift_i1 [lemma, in Presburger.Lift]
iso_iso3_2 [lemma, in Presburger.Lift]
iso_iso3_1 [lemma, in Presburger.Lift]
iso_list3 [definition, in Presburger.Lift]
iso_shiftForm [lemma, in Presburger.Lift]
iso_shiftExp [lemma, in Presburger.Lift]
iso_list [definition, in Presburger.Lift]
iso3_2 [lemma, in Presburger.Lift]
iso3_1 [lemma, in Presburger.Lift]
L
lcm [definition, in Presburger.Nat]lcm_lt_O [lemma, in Presburger.Nat]
lcm_sym [lemma, in Presburger.Nat]
le_ind2 [lemma, in Presburger.Nat]
Lift [library]
lift_quant_groundN [lemma, in Presburger.Lift]
lift_quant_prenex [lemma, in Presburger.Lift]
lift_quant [definition, in Presburger.Lift]
lift_neg_groundN [lemma, in Presburger.Lift]
lift_neg_prenex [lemma, in Presburger.Lift]
lift_neg [definition, in Presburger.Lift]
lift_andor_or_groundN [lemma, in Presburger.Lift]
lift_andor_and_groundN [lemma, in Presburger.Lift]
lift_andor2_or_groundN [lemma, in Presburger.Lift]
lift_andor2_and_groundN [lemma, in Presburger.Lift]
lift_andor1_or_groundN [lemma, in Presburger.Lift]
lift_andor1_and_groundN [lemma, in Presburger.Lift]
lift_andor_prenex [lemma, in Presburger.Lift]
lift_andor2_prenex [lemma, in Presburger.Lift]
lift_andor1_prenex [lemma, in Presburger.Lift]
lift_andor1_noBinder [lemma, in Presburger.Lift]
lift_andor [definition, in Presburger.Lift]
lift_andor2 [definition, in Presburger.Lift]
lift_andor1 [definition, in Presburger.Lift]
lift_if_groundN [lemma, in Presburger.Lift]
lift_if_prenex [lemma, in Presburger.Lift]
lift_if2_groundN [lemma, in Presburger.Lift]
lift_if2_prenex [lemma, in Presburger.Lift]
lift_if1_groundN [lemma, in Presburger.Lift]
lift_if1_prenex [lemma, in Presburger.Lift]
lift_if1_noBinder [lemma, in Presburger.Lift]
lift_if [definition, in Presburger.Lift]
lift_if2 [definition, in Presburger.Lift]
lift_if1 [definition, in Presburger.Lift]
listCongP [inductive, in Presburger.Form]
listCongPcons [constructor, in Presburger.Form]
listCongPnil [constructor, in Presburger.Form]
listCong_app [lemma, in Presburger.Form]
listEqP [inductive, in Presburger.Form]
listEqPcons [constructor, in Presburger.Form]
listEqPnil [constructor, in Presburger.Form]
listEq_app [lemma, in Presburger.Form]
listNEqP [inductive, in Presburger.Form]
listNEqPcons [constructor, in Presburger.Form]
listNEqPnil [constructor, in Presburger.Form]
listNeq_app [lemma, in Presburger.Form]
ltdec [definition, in Presburger.Nat]
ltdec_correct [lemma, in Presburger.Nat]
lt_inj [lemma, in Presburger.Cong]
M
maxC [definition, in Presburger.Process]maxCPos [lemma, in Presburger.Process]
maxL [definition, in Presburger.Process]
maxPos [lemma, in Presburger.Process]
max_Or [lemma, in Presburger.Nat]
minus_O_le [lemma, in Presburger.Nat]
minus_O [lemma, in Presburger.Nat]
minus2 [definition, in Presburger.Nat]
minus2_correct [lemma, in Presburger.Nat]
mult_lt_ZERO [lemma, in Presburger.Nat]
mult_inv1 [lemma, in Presburger.Nat]
mult_inv [lemma, in Presburger.Nat]
N
Nat [library]nBAnd [constructor, in Presburger.Form]
nBCong [constructor, in Presburger.Form]
nBEq [constructor, in Presburger.Form]
nBFalse [constructor, in Presburger.Form]
nBImp [constructor, in Presburger.Form]
nBNeg [constructor, in Presburger.Form]
nBOr [constructor, in Presburger.Form]
nBTrue [constructor, in Presburger.Form]
nCnf [constructor, in Presburger.Normal]
NDivides_minus [lemma, in Presburger.Zdivides]
Neg [constructor, in Presburger.Form]
neg_cong [lemma, in Presburger.Cong]
nExists [constructor, in Presburger.Normal]
nNExists [constructor, in Presburger.Normal]
noBinder [inductive, in Presburger.Form]
noBinder_Neg [lemma, in Presburger.Normal]
noBinder_shift [lemma, in Presburger.Lift]
NOddEven [lemma, in Presburger.PresTac_ex]
NOddEven [lemma, in Presburger.Elim]
None [constructor, in Presburger.Option]
Normal [inductive, in Presburger.Normal]
Normal [library]
normalForm [definition, in Presburger.Normal]
normalForm_groundN [lemma, in Presburger.Normal]
normalForm_correct [lemma, in Presburger.Normal]
normal_normal [lemma, in Presburger.Normal]
Num [constructor, in Presburger.Form]
O
OddEven [lemma, in Presburger.PresTac_ex]OddEven [lemma, in Presburger.Elim]
oneCongNeq_correct [lemma, in Presburger.Process]
onlyNeg_correct_aux2 [lemma, in Presburger.Process]
onlyNeg_correct_aux1 [lemma, in Presburger.Process]
onlyNeg_correct [lemma, in Presburger.Process]
onlyNeg_correct_aux [lemma, in Presburger.Process]
Option [inductive, in Presburger.Option]
Option [library]
Or [constructor, in Presburger.Form]
oZ [definition, in Presburger.Zdivides]
oZ1 [definition, in Presburger.Zdivides]
P
Pdiv [definition, in Presburger.Zdivides]Pdiv_correct [lemma, in Presburger.Zdivides]
pExists [constructor, in Presburger.Lift]
pForall [constructor, in Presburger.Lift]
Plus [constructor, in Presburger.Form]
PNeg [inductive, in Presburger.Normal]
PNegAnd [constructor, in Presburger.Normal]
PNegCnf2 [constructor, in Presburger.Normal]
PNegOr [constructor, in Presburger.Normal]
pNoBinder [constructor, in Presburger.Lift]
pos_eq_bool_correct [lemma, in Presburger.Zdivides]
pos_eq_bool [definition, in Presburger.Zdivides]
POS_inject [lemma, in Presburger.Zdivides]
pred_le [lemma, in Presburger.Nat]
prenex [inductive, in Presburger.Lift]
presburger [definition, in Presburger.Elim]
presburger_correct [lemma, in Presburger.Elim]
PresTac [library]
PresTac_ex [library]
Process [library]
processList [definition, in Presburger.Process]
processList_groundN [lemma, in Presburger.Process]
processList_correct [lemma, in Presburger.Process]
ptonat_def1 [lemma, in Presburger.Zdivides]
push_and_groundN [lemma, in Presburger.Normal]
push_and_correct [lemma, in Presburger.Normal]
push_and_cnf [lemma, in Presburger.Normal]
push_and_rules_groundN [lemma, in Presburger.Normal]
push_and_rules_correct [lemma, in Presburger.Normal]
push_and_rules_cnf [lemma, in Presburger.Normal]
push_and_rules1_groundN [lemma, in Presburger.Normal]
push_and_rules1_correct [lemma, in Presburger.Normal]
push_and_rules1_cnf [lemma, in Presburger.Normal]
push_and [definition, in Presburger.Normal]
push_and_rules [definition, in Presburger.Normal]
push_and_rules1 [definition, in Presburger.Normal]
push_neg_groundN [lemma, in Presburger.Normal]
push_neg_correct [lemma, in Presburger.Normal]
push_neg_pneg [lemma, in Presburger.Normal]
push_neg [definition, in Presburger.Normal]
R
ReduceCong [library]reduceCongCong [definition, in Presburger.ReduceCong]
reduceCongCong_groundN [lemma, in Presburger.ReduceCong]
reduceCongCong_correct [lemma, in Presburger.ReduceCong]
reduceCongCong1 [definition, in Presburger.ReduceCong]
reduceCongCong1_groundN [lemma, in Presburger.ReduceCong]
reduceCongCong1_correct [lemma, in Presburger.ReduceCong]
ReduceEq [library]
reduceEqCong [definition, in Presburger.ReduceEq]
reduceEqCong_groundN [lemma, in Presburger.ReduceEq]
reduceEqCong_correct [lemma, in Presburger.ReduceEq]
reduceEqEq [definition, in Presburger.ReduceEq]
reduceEqEq_groundN [lemma, in Presburger.ReduceEq]
reduceEqEq_correct [lemma, in Presburger.ReduceEq]
reduceEqNEq [definition, in Presburger.ReduceEq]
reduceEqNEq_groundN [lemma, in Presburger.ReduceEq]
reduceEqNEq_correct [lemma, in Presburger.ReduceEq]
S
scal [definition, in Presburger.Form]scal_correct [lemma, in Presburger.Form]
scal_groundN [lemma, in Presburger.GroundN]
shiftExp [definition, in Presburger.Form]
shiftExp_groundN [lemma, in Presburger.GroundN]
shiftForm [definition, in Presburger.Form]
shiftForm_groundN [lemma, in Presburger.GroundN]
Some [constructor, in Presburger.Option]
Sort [library]
sortAnd [definition, in Presburger.Sort]
sortAnd_groundN [lemma, in Presburger.Sort]
sortAnd_correct [lemma, in Presburger.Sort]
sTactic [library]
T
TRue [constructor, in Presburger.Form]V
Var [constructor, in Presburger.Form]Z
Zabs_absolu [lemma, in Presburger.Cong]Zabs_tri [lemma, in Presburger.Zdivides]
Zabs_intro [lemma, in Presburger.Zdivides]
Zabs_eq_case [lemma, in Presburger.Zdivides]
Zabs_Zmult [lemma, in Presburger.Zdivides]
Zabs_Zopp [lemma, in Presburger.Zdivides]
Zdivides [definition, in Presburger.Zdivides]
Zdivides [library]
ZdividesDiv [lemma, in Presburger.Zdivides]
ZDividesLe [lemma, in Presburger.Zdivides]
ZdividesMult [lemma, in Presburger.Zdivides]
ZdividesP [definition, in Presburger.Zdivides]
ZdividesTrans [lemma, in Presburger.Zdivides]
ZdividesZquotient [lemma, in Presburger.Zdivides]
ZdividesZquotientInv [lemma, in Presburger.Zdivides]
ZDivides_mult [lemma, in Presburger.Zdivides]
ZDivides_add [lemma, in Presburger.Zdivides]
Zdivides1 [lemma, in Presburger.Zdivides]
Zeq_mult_simpl [lemma, in Presburger.Zdivides]
Zero_le_oZ [lemma, in Presburger.Zdivides]
Zle_NEG_POS [lemma, in Presburger.Zdivides]
Zle_Zabs [lemma, in Presburger.Zdivides]
Zlt_ZERO_minus [lemma, in Presburger.Cong]
Zmax [definition, in Presburger.Zdivides]
Zmax1 [lemma, in Presburger.Zdivides]
Zmax2 [lemma, in Presburger.Zdivides]
Zquotient [definition, in Presburger.Zdivides]
ZquotientMonotone [lemma, in Presburger.Zdivides]
ZquotientPos [lemma, in Presburger.Zdivides]
ZquotientProp [lemma, in Presburger.Zdivides]
ZquotientUnique [lemma, in Presburger.Zdivides]
ZquotientZopp [lemma, in Presburger.Zdivides]
Zquotient_mult_comp [lemma, in Presburger.Zdivides]
Zquotient1 [lemma, in Presburger.Zdivides]
Z_eq_bool_correct [lemma, in Presburger.Zdivides]
Z_eq_bool [definition, in Presburger.Zdivides]
Z_O_1 [lemma, in Presburger.Zdivides]
Library Index
C
CongE
ElimF
FactorForm
G
GroundNL
LiftN
NatNormal
O
OptionP
PresTacPresTac_ex
Process
R
ReduceCongReduceEq
S
SortsTactic
Z
ZdividesLemma Index
B
buildConj_append [in Presburger.Form]C
cnf_noBinder [in Presburger.Elim]cnf_groundN [in Presburger.Normal]
cnf_correct [in Presburger.Normal]
cnf_cnf [in Presburger.Normal]
Cnf1_cons [in Presburger.Normal]
Cnf1_app [in Presburger.Normal]
congZ_O_Eq [in Presburger.Cong]
congZ_mult [in Presburger.Cong]
congZ_minus [in Presburger.Cong]
congZ_plus [in Presburger.Cong]
congZ_trans [in Presburger.Cong]
congZ_sym [in Presburger.Cong]
congZ_id [in Presburger.Cong]
Contradict1 [in Presburger.sTactic]
Contradict2 [in Presburger.sTactic]
Contradict3 [in Presburger.sTactic]
correct_lift_quant [in Presburger.Lift]
correct_lift_neg [in Presburger.Lift]
correct_lift_andor_or [in Presburger.Lift]
correct_lift_andor_and [in Presburger.Lift]
correct_lift_if [in Presburger.Lift]
D
decideCorrect [in Presburger.Form]divides_lcm3 [in Presburger.Nat]
divides_lcm2 [in Presburger.Nat]
divides_lcm1 [in Presburger.Nat]
divides_div [in Presburger.Nat]
divides_id [in Presburger.Nat]
divides_gcd3 [in Presburger.Nat]
divides_gcd1_aux [in Presburger.Nat]
divides_gcd2 [in Presburger.Nat]
divides_gcd1 [in Presburger.Nat]
divides_gcd_aux [in Presburger.Nat]
divides_minus [in Presburger.Nat]
divides_add [in Presburger.Nat]
divides_trans [in Presburger.Nat]
divides_refl [in Presburger.Nat]
div_lt_ZERO [in Presburger.Nat]
div_correct [in Presburger.Nat]
div1_correct [in Presburger.Nat]
E
econg_pneg [in Presburger.Normal]econg_groundN [in Presburger.Normal]
econg_correct [in Presburger.Normal]
elimQuants_groundN [in Presburger.Elim]
elimQuants_correct [in Presburger.Elim]
elimQuant_groundN [in Presburger.Elim]
elimQuant_correct [in Presburger.Elim]
expand_forall_groundN [in Presburger.Normal]
expand_forall_correct [in Presburger.Normal]
expand_forall_normal [in Presburger.Normal]
expand_groundN [in Presburger.Normal]
expand_cong_correct [in Presburger.Normal]
expand_cong_pneg [in Presburger.Normal]
exp2Z_ground [in Presburger.Form]
F
factorExp_groundN [in Presburger.Factor]factorExp_correct [in Presburger.Factor]
factorVar0_groundN [in Presburger.Factor]
factorVar0_correct [in Presburger.Factor]
fcong_correct [in Presburger.Cong]
fgrounNExp_correct [in Presburger.GroundN]
fgrounNForm_correct [in Presburger.GroundN]
formL2Prop_append [in Presburger.Form]
form2Prop_app_inv [in Presburger.Form]
form2Prop_cons_inv [in Presburger.Form]
form2Prop_app [in Presburger.Form]
form2Prop_cons [in Presburger.Form]
G
gcd_lt_zero [in Presburger.Nat]gcd_sym [in Presburger.Nat]
gcd_bezout [in Presburger.Nat]
gcd_O2 [in Presburger.Nat]
gcd_O1 [in Presburger.Nat]
gcd1_O [in Presburger.Nat]
gcd1_bezout [in Presburger.Nat]
gcd1_bezout1 [in Presburger.Nat]
gcd1_bezout0 [in Presburger.Nat]
groundNExp_le [in Presburger.GroundN]
groundNForm_Cnf_groundForm_aux [in Presburger.Elim]
groundNForm_le [in Presburger.GroundN]
groundNL_groundNForm [in Presburger.Elim]
groundNL_le [in Presburger.GroundN]
groundNL_app [in Presburger.GroundN]
groundNL2_le [in Presburger.GroundN]
groundNL2_app [in Presburger.GroundN]
I
inj_oZ1 [in Presburger.Zdivides]iso_lift_andor_or2 [in Presburger.Lift]
iso_lift_andor_and2 [in Presburger.Lift]
iso_lift_andor_or1 [in Presburger.Lift]
iso_lift_andor_and1 [in Presburger.Lift]
iso_lift_i2 [in Presburger.Lift]
iso_lift_i1 [in Presburger.Lift]
iso_iso3_2 [in Presburger.Lift]
iso_iso3_1 [in Presburger.Lift]
iso_shiftForm [in Presburger.Lift]
iso_shiftExp [in Presburger.Lift]
iso3_2 [in Presburger.Lift]
iso3_1 [in Presburger.Lift]
L
lcm_lt_O [in Presburger.Nat]lcm_sym [in Presburger.Nat]
le_ind2 [in Presburger.Nat]
lift_quant_groundN [in Presburger.Lift]
lift_quant_prenex [in Presburger.Lift]
lift_neg_groundN [in Presburger.Lift]
lift_neg_prenex [in Presburger.Lift]
lift_andor_or_groundN [in Presburger.Lift]
lift_andor_and_groundN [in Presburger.Lift]
lift_andor2_or_groundN [in Presburger.Lift]
lift_andor2_and_groundN [in Presburger.Lift]
lift_andor1_or_groundN [in Presburger.Lift]
lift_andor1_and_groundN [in Presburger.Lift]
lift_andor_prenex [in Presburger.Lift]
lift_andor2_prenex [in Presburger.Lift]
lift_andor1_prenex [in Presburger.Lift]
lift_andor1_noBinder [in Presburger.Lift]
lift_if_groundN [in Presburger.Lift]
lift_if_prenex [in Presburger.Lift]
lift_if2_groundN [in Presburger.Lift]
lift_if2_prenex [in Presburger.Lift]
lift_if1_groundN [in Presburger.Lift]
lift_if1_prenex [in Presburger.Lift]
lift_if1_noBinder [in Presburger.Lift]
listCong_app [in Presburger.Form]
listEq_app [in Presburger.Form]
listNeq_app [in Presburger.Form]
ltdec_correct [in Presburger.Nat]
lt_inj [in Presburger.Cong]
M
maxCPos [in Presburger.Process]maxPos [in Presburger.Process]
max_Or [in Presburger.Nat]
minus_O_le [in Presburger.Nat]
minus_O [in Presburger.Nat]
minus2_correct [in Presburger.Nat]
mult_lt_ZERO [in Presburger.Nat]
mult_inv1 [in Presburger.Nat]
mult_inv [in Presburger.Nat]
N
NDivides_minus [in Presburger.Zdivides]neg_cong [in Presburger.Cong]
noBinder_Neg [in Presburger.Normal]
noBinder_shift [in Presburger.Lift]
NOddEven [in Presburger.PresTac_ex]
NOddEven [in Presburger.Elim]
normalForm_groundN [in Presburger.Normal]
normalForm_correct [in Presburger.Normal]
normal_normal [in Presburger.Normal]
O
OddEven [in Presburger.PresTac_ex]OddEven [in Presburger.Elim]
oneCongNeq_correct [in Presburger.Process]
onlyNeg_correct_aux2 [in Presburger.Process]
onlyNeg_correct_aux1 [in Presburger.Process]
onlyNeg_correct [in Presburger.Process]
onlyNeg_correct_aux [in Presburger.Process]
P
Pdiv_correct [in Presburger.Zdivides]pos_eq_bool_correct [in Presburger.Zdivides]
POS_inject [in Presburger.Zdivides]
pred_le [in Presburger.Nat]
presburger_correct [in Presburger.Elim]
processList_groundN [in Presburger.Process]
processList_correct [in Presburger.Process]
ptonat_def1 [in Presburger.Zdivides]
push_and_groundN [in Presburger.Normal]
push_and_correct [in Presburger.Normal]
push_and_cnf [in Presburger.Normal]
push_and_rules_groundN [in Presburger.Normal]
push_and_rules_correct [in Presburger.Normal]
push_and_rules_cnf [in Presburger.Normal]
push_and_rules1_groundN [in Presburger.Normal]
push_and_rules1_correct [in Presburger.Normal]
push_and_rules1_cnf [in Presburger.Normal]
push_neg_groundN [in Presburger.Normal]
push_neg_correct [in Presburger.Normal]
push_neg_pneg [in Presburger.Normal]
R
reduceCongCong_groundN [in Presburger.ReduceCong]reduceCongCong_correct [in Presburger.ReduceCong]
reduceCongCong1_groundN [in Presburger.ReduceCong]
reduceCongCong1_correct [in Presburger.ReduceCong]
reduceEqCong_groundN [in Presburger.ReduceEq]
reduceEqCong_correct [in Presburger.ReduceEq]
reduceEqEq_groundN [in Presburger.ReduceEq]
reduceEqEq_correct [in Presburger.ReduceEq]
reduceEqNEq_groundN [in Presburger.ReduceEq]
reduceEqNEq_correct [in Presburger.ReduceEq]
S
scal_correct [in Presburger.Form]scal_groundN [in Presburger.GroundN]
shiftExp_groundN [in Presburger.GroundN]
shiftForm_groundN [in Presburger.GroundN]
sortAnd_groundN [in Presburger.Sort]
sortAnd_correct [in Presburger.Sort]
Z
Zabs_absolu [in Presburger.Cong]Zabs_tri [in Presburger.Zdivides]
Zabs_intro [in Presburger.Zdivides]
Zabs_eq_case [in Presburger.Zdivides]
Zabs_Zmult [in Presburger.Zdivides]
Zabs_Zopp [in Presburger.Zdivides]
ZdividesDiv [in Presburger.Zdivides]
ZDividesLe [in Presburger.Zdivides]
ZdividesMult [in Presburger.Zdivides]
ZdividesTrans [in Presburger.Zdivides]
ZdividesZquotient [in Presburger.Zdivides]
ZdividesZquotientInv [in Presburger.Zdivides]
ZDivides_mult [in Presburger.Zdivides]
ZDivides_add [in Presburger.Zdivides]
Zdivides1 [in Presburger.Zdivides]
Zeq_mult_simpl [in Presburger.Zdivides]
Zero_le_oZ [in Presburger.Zdivides]
Zle_NEG_POS [in Presburger.Zdivides]
Zle_Zabs [in Presburger.Zdivides]
Zlt_ZERO_minus [in Presburger.Cong]
Zmax1 [in Presburger.Zdivides]
Zmax2 [in Presburger.Zdivides]
ZquotientMonotone [in Presburger.Zdivides]
ZquotientPos [in Presburger.Zdivides]
ZquotientProp [in Presburger.Zdivides]
ZquotientUnique [in Presburger.Zdivides]
ZquotientZopp [in Presburger.Zdivides]
Zquotient_mult_comp [in Presburger.Zdivides]
Zquotient1 [in Presburger.Zdivides]
Z_eq_bool_correct [in Presburger.Zdivides]
Z_O_1 [in Presburger.Zdivides]
Constructor Index
A
ANd [in Presburger.Form]C
CnfCnf1 [in Presburger.Normal]CnfOr [in Presburger.Normal]
Cnf1And [in Presburger.Normal]
Cnf1Cnf2 [in Presburger.Normal]
Cnf2Cong [in Presburger.Normal]
Cnf2Eq [in Presburger.Normal]
Cnf2False [in Presburger.Normal]
Cnf2NEq [in Presburger.Normal]
Cnf2True [in Presburger.Normal]
Cong [in Presburger.Form]
E
Eq [in Presburger.Form]Exists [in Presburger.Form]
F
FAlse [in Presburger.Form]Forall [in Presburger.Form]
G
GAnd [in Presburger.Form]GCong [in Presburger.Form]
GEq [in Presburger.Form]
GFalse [in Presburger.Form]
GImp [in Presburger.Form]
GNAnd [in Presburger.GroundN]
GNCong [in Presburger.GroundN]
GNeg [in Presburger.Form]
GNEq [in Presburger.GroundN]
GNExists [in Presburger.GroundN]
GNFalse [in Presburger.GroundN]
GNForall [in Presburger.GroundN]
GNImp [in Presburger.GroundN]
GNNeg [in Presburger.GroundN]
GNNil [in Presburger.GroundN]
GNNil2 [in Presburger.GroundN]
GNNum [in Presburger.GroundN]
GNOr [in Presburger.GroundN]
GNPlus [in Presburger.GroundN]
GNTrue [in Presburger.GroundN]
GNum [in Presburger.Form]
GNVar [in Presburger.GroundN]
GNVCons [in Presburger.GroundN]
GNVCons2 [in Presburger.GroundN]
GOr [in Presburger.Form]
GPlus [in Presburger.Form]
GTrue [in Presburger.Form]
I
Imp [in Presburger.Form]L
listCongPcons [in Presburger.Form]listCongPnil [in Presburger.Form]
listEqPcons [in Presburger.Form]
listEqPnil [in Presburger.Form]
listNEqPcons [in Presburger.Form]
listNEqPnil [in Presburger.Form]
N
nBAnd [in Presburger.Form]nBCong [in Presburger.Form]
nBEq [in Presburger.Form]
nBFalse [in Presburger.Form]
nBImp [in Presburger.Form]
nBNeg [in Presburger.Form]
nBOr [in Presburger.Form]
nBTrue [in Presburger.Form]
nCnf [in Presburger.Normal]
Neg [in Presburger.Form]
nExists [in Presburger.Normal]
nNExists [in Presburger.Normal]
None [in Presburger.Option]
Num [in Presburger.Form]
O
Or [in Presburger.Form]P
pExists [in Presburger.Lift]pForall [in Presburger.Lift]
Plus [in Presburger.Form]
PNegAnd [in Presburger.Normal]
PNegCnf2 [in Presburger.Normal]
PNegOr [in Presburger.Normal]
pNoBinder [in Presburger.Lift]
S
Some [in Presburger.Option]T
TRue [in Presburger.Form]V
Var [in Presburger.Form]Inductive Index
C
Cnf [in Presburger.Normal]Cnf1 [in Presburger.Normal]
Cnf2 [in Presburger.Normal]
E
exp [in Presburger.Form]F
form [in Presburger.Form]G
groundExp [in Presburger.Form]groundForm [in Presburger.Form]
groundNExp [in Presburger.GroundN]
groundNForm [in Presburger.GroundN]
groundNL [in Presburger.GroundN]
groundNL2 [in Presburger.GroundN]
L
listCongP [in Presburger.Form]listEqP [in Presburger.Form]
listNEqP [in Presburger.Form]
N
noBinder [in Presburger.Form]Normal [in Presburger.Normal]
O
Option [in Presburger.Option]P
PNeg [in Presburger.Normal]prenex [in Presburger.Lift]
Definition Index
B
buildConj [in Presburger.Form]C
cnf [in Presburger.Normal]congZ [in Presburger.Cong]
congZ_dec [in Presburger.Cong]
D
decideGround [in Presburger.Form]div [in Presburger.Nat]
divides [in Presburger.Nat]
div1 [in Presburger.Nat]
E
econg [in Presburger.Normal]elimQuant [in Presburger.Elim]
elimQuants [in Presburger.Elim]
expand_forall [in Presburger.Normal]
expand_cong [in Presburger.Normal]
exp2Z [in Presburger.Form]
F
factorExp [in Presburger.Factor]factorVar0 [in Presburger.Factor]
fcong [in Presburger.Cong]
fgroundNExp [in Presburger.GroundN]
fgroundNForm [in Presburger.GroundN]
formL2Prop [in Presburger.Form]
form2Prop [in Presburger.Form]
G
gcd [in Presburger.Nat]gcd1 [in Presburger.Nat]
I
iso_list3 [in Presburger.Lift]iso_list [in Presburger.Lift]
L
lcm [in Presburger.Nat]lift_quant [in Presburger.Lift]
lift_neg [in Presburger.Lift]
lift_andor [in Presburger.Lift]
lift_andor2 [in Presburger.Lift]
lift_andor1 [in Presburger.Lift]
lift_if [in Presburger.Lift]
lift_if2 [in Presburger.Lift]
lift_if1 [in Presburger.Lift]
ltdec [in Presburger.Nat]
M
maxC [in Presburger.Process]maxL [in Presburger.Process]
minus2 [in Presburger.Nat]
N
normalForm [in Presburger.Normal]O
oZ [in Presburger.Zdivides]oZ1 [in Presburger.Zdivides]
P
Pdiv [in Presburger.Zdivides]pos_eq_bool [in Presburger.Zdivides]
presburger [in Presburger.Elim]
processList [in Presburger.Process]
push_and [in Presburger.Normal]
push_and_rules [in Presburger.Normal]
push_and_rules1 [in Presburger.Normal]
push_neg [in Presburger.Normal]
R
reduceCongCong [in Presburger.ReduceCong]reduceCongCong1 [in Presburger.ReduceCong]
reduceEqCong [in Presburger.ReduceEq]
reduceEqEq [in Presburger.ReduceEq]
reduceEqNEq [in Presburger.ReduceEq]
S
scal [in Presburger.Form]shiftExp [in Presburger.Form]
shiftForm [in Presburger.Form]
sortAnd [in Presburger.Sort]
Z
Zdivides [in Presburger.Zdivides]ZdividesP [in Presburger.Zdivides]
Zmax [in Presburger.Zdivides]
Zquotient [in Presburger.Zdivides]
Z_eq_bool [in Presburger.Zdivides]
| 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 | (390 entries) |
| 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 | (17 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 | (217 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 | (74 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 | (19 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 | (63 entries) |