Global Index

H

J

K

O

Q

V

W

X

Y

Z

_

(797 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(33 entries)

Module Index

A

B

C

D

G

H

I

J

K

L

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(16 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(8 entries)

Library Index

A

B

C

F

G

H

J

K

L

N

O

P

Q

T

V

W

X

Y

Z

_

other

(11 entries)

Lemma Index

B

C

D

H

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

other

(373 entries)

Axiom Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(12 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(149 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(23 entries)

Instance Index

A

B

C

D

E

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(11 entries)

Definition Index

A

H

I

J

K

O

P

Q

R

U

V

W

X

Y

Z

_

other

(147 entries)

Global Index

A

AtomNotInTheory [lemma, in BioFLL.Utils]

B

bleccm0 [definition, in BioFLL.Definitions]
bleccm1 [definition, in BioFLL.Definitions]
bleccm2 [definition, in BioFLL.Definitions]
blecc0 [definition, in BioFLL.Definitions]
blecc1 [definition, in BioFLL.Definitions]
blecc2 [definition, in BioFLL.Definitions]
blecm0 [definition, in BioFLL.Definitions]
blecm1 [definition, in BioFLL.Definitions]
blecm2 [definition, in BioFLL.Definitions]
blec0 [definition, in BioFLL.Definitions]
blec1 [definition, in BioFLL.Definitions]
blec2 [definition, in BioFLL.Definitions]
blec3 [definition, in BioFLL.Definitions]
ble0 [definition, in BioFLL.Definitions]
ble0r [definition, in BioFLL.Definitions]
ble1 [definition, in BioFLL.Definitions]
ble2 [definition, in BioFLL.Definitions]
blood [definition, in BioFLL.Definitions]
bone [definition, in BioFLL.Definitions]
bo0 [definition, in BioFLL.Definitions]
bo1 [definition, in BioFLL.Definitions]
bo2 [definition, in BioFLL.Definitions]
breast [definition, in BioFLL.Definitions]
bre0 [definition, in BioFLL.Definitions]
bre0r [definition, in BioFLL.Definitions]
bre1 [definition, in BioFLL.Definitions]
bre2 [definition, in BioFLL.Definitions]
brt0 [definition, in BioFLL.Definitions]
brt0r [definition, in BioFLL.Definitions]
brt1 [definition, in BioFLL.Definitions]
brt2 [definition, in BioFLL.Definitions]
br0 [definition, in BioFLL.Definitions]
br1 [definition, in BioFLL.Definitions]
br2 [definition, in BioFLL.Definitions]

C

CD44 [definition, in BioFLL.Definitions]
CD47 [definition, in BioFLL.Definitions]

D

Definitions [library]
d00 [definition, in BioFLL.Definitions]
d01 [definition, in BioFLL.Definitions]
d02 [definition, in BioFLL.Definitions]
d10 [definition, in BioFLL.Definitions]
d10r [definition, in BioFLL.Definitions]
d11 [definition, in BioFLL.Definitions]
d12 [definition, in BioFLL.Definitions]
d20 [definition, in BioFLL.Definitions]
d20r [definition, in BioFLL.Definitions]
d21 [definition, in BioFLL.Definitions]
d22 [definition, in BioFLL.Definitions]
d30 [definition, in BioFLL.Definitions]
d30r [definition, in BioFLL.Definitions]
d31 [definition, in BioFLL.Definitions]
d32 [definition, in BioFLL.Definitions]
d40 [definition, in BioFLL.Definitions]
d41 [definition, in BioFLL.Definitions]
d42 [definition, in BioFLL.Definitions]
d43 [definition, in BioFLL.Definitions]
d50 [definition, in BioFLL.Definitions]
d51 [definition, in BioFLL.Definitions]
d52 [definition, in BioFLL.Definitions]
d60 [definition, in BioFLL.Definitions]
d61 [definition, in BioFLL.Definitions]
d62 [definition, in BioFLL.Definitions]
d70 [definition, in BioFLL.Definitions]
d71 [definition, in BioFLL.Definitions]
d72 [definition, in BioFLL.Definitions]
d80 [definition, in BioFLL.Definitions]
d81 [definition, in BioFLL.Definitions]
d82 [definition, in BioFLL.Definitions]

E

EncodeRule [definition, in BioFLL.Definitions]
EncodeRuleAP [definition, in BioFLL.Definitions]
EP [definition, in BioFLL.Definitions]
EPCAM [definition, in BioFLL.Definitions]
EPCD [definition, in BioFLL.Definitions]
EPCDCD [definition, in BioFLL.Definitions]
EPCDCDME [definition, in BioFLL.Definitions]
EPCDCDMEse [definition, in BioFLL.Definitions]
EPCDME [definition, in BioFLL.Definitions]
EqC [lemma, in BioFLL.Utils]
EqL [lemma, in BioFLL.Utils]
Eqset [module, in BioFLL.LL.Eqset]
Eqset [library]
Eqset_dec_pol.isPositive [axiom, in BioFLL.LL.Eqset]
Eqset_dec_pol.eqA_dec [axiom, in BioFLL.LL.Eqset]
Eqset_dec_pol.A [axiom, in BioFLL.LL.Eqset]
Eqset_dec_pol [module, in BioFLL.LL.Eqset]
Eqset_dec.eqA_dec [axiom, in BioFLL.LL.Eqset]
Eqset_dec.A [axiom, in BioFLL.LL.Eqset]
Eqset_dec [module, in BioFLL.LL.Eqset]
Eqset.A [axiom, in BioFLL.LL.Eqset]
EqT [lemma, in BioFLL.Utils]
EqTFC [lemma, in BioFLL.Utils]
ExTXT [lemma, in BioFLL.Utils]

F

FocusAtom [lemma, in BioFLL.InversionTactics]
FocusOnlyTheory [lemma, in BioFLL.Utils]
FocusonParAtom [lemma, in BioFLL.InversionTactics]
FocusTensorAtom [lemma, in BioFLL.InversionTactics]
FormulasLL [module, in BioFLL.LL.Syntax]
FormulasLL.LexpPosConc [lemma, in BioFLL.LL.Syntax]
FormulasLL.LexpPosCons [lemma, in BioFLL.LL.Syntax]
FormulasLL.LexpPosOrNegAtomConc [lemma, in BioFLL.LL.Syntax]
FormulasLL.lexpPos_morph [instance, in BioFLL.LL.Syntax]
FormulasLL.lexp_eq.eqA_dec [definition, in BioFLL.LL.Syntax]
FormulasLL.lexp_eq.A [definition, in BioFLL.LL.Syntax]
FormulasLL.lexp_eq [module, in BioFLL.LL.Syntax]
FormulasLL.LPos1 [lemma, in BioFLL.LL.Syntax]
FormulasLL.LPos2 [lemma, in BioFLL.LL.Syntax]
FormulasLL.LPos3 [lemma, in BioFLL.LL.Syntax]
FormulasLL.MSetList [module, in BioFLL.LL.Syntax]
FormulasLL.Sy [module, in BioFLL.LL.Syntax]

G

GenRs [definition, in BioFLL.Definitions]
GoalP5 [definition, in BioFLL.MetaLevelProperties]
GtZero [lemma, in BioFLL.LL.Eqset]

I

InMeq [lemma, in BioFLL.Utils]
InversionTactics [library]
InvRuleTheory [lemma, in BioFLL.InversionTactics]
InvRuleTheoryAp [lemma, in BioFLL.InversionTactics]

L

ListPosAtom [definition, in BioFLL.Utils]

M

MET [definition, in BioFLL.Definitions]
MetaLevelProperties [library]
MultisetList [module, in BioFLL.LL.Multisets]
MultisetList.aunion_comm [lemma, in BioFLL.LL.Multisets]
MultisetList.axPair [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_In [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_cons_neq [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_cons_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_inv_nil [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_not_In [lemma, in BioFLL.LL.Multisets]
MultisetList.countIn_nil [lemma, in BioFLL.LL.Multisets]
MultisetList.Decidability [section, in BioFLL.LL.Multisets]
MultisetList.DestructMSet [lemma, in BioFLL.LL.Multisets]
MultisetList.DestructMSet' [lemma, in BioFLL.LL.Multisets]
MultisetList.DestructMSet2 [lemma, in BioFLL.LL.Multisets]
MultisetList.DestructMSet2_aux [lemma, in BioFLL.LL.Multisets]
MultisetList.DestructMSet2' [lemma, in BioFLL.LL.Multisets]
MultisetList.DestructMulFalse [lemma, in BioFLL.LL.Multisets]
MultisetList.diff [definition, in BioFLL.LL.Multisets]
MultisetList.diff_MM_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_remove_both [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_member_ly_rn [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_morph [instance, in BioFLL.LL.Multisets]
MultisetList.diff_mult [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_mult_step_neq [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_mult_step_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_perm [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_perm_single [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_mult_comp [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_empty_r [lemma, in BioFLL.LL.Multisets]
MultisetList.diff_empty_l [lemma, in BioFLL.LL.Multisets]
MultisetList.empty [definition, in BioFLL.LL.Multisets]
MultisetList.EmptyMS [lemma, in BioFLL.LL.Multisets]
MultisetList.empty_decomp_dec [lemma, in BioFLL.LL.Multisets]
MultisetList.empty_dec [lemma, in BioFLL.LL.Multisets]
MultisetList.empty_mult [lemma, in BioFLL.LL.Multisets]
MultisetList.empty_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.emp_mult [lemma, in BioFLL.LL.Multisets]
MultisetList.eq_then_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.eq_step [lemma, in BioFLL.LL.Multisets]
MultisetList.insert_remove_noteq [lemma, in BioFLL.LL.Multisets]
MultisetList.insert_remove_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.insert_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.insert_morph [instance, in BioFLL.LL.Multisets]
MultisetList.ins_meq_union [lemma, in BioFLL.LL.Multisets]
MultisetList.In_to_in [lemma, in BioFLL.LL.Multisets]
MultisetList.In_union_or' [lemma, in BioFLL.LL.Multisets]
MultisetList.In_union_or [lemma, in BioFLL.LL.Multisets]
MultisetList.in_countIn [lemma, in BioFLL.LL.Multisets]
MultisetList.lenghtList [lemma, in BioFLL.LL.Multisets]
MultisetList.member [definition, in BioFLL.LL.Multisets]
MultisetList.member_due [lemma, in BioFLL.LL.Multisets]
MultisetList.member_unit [lemma, in BioFLL.LL.Multisets]
MultisetList.member_then_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.member_then_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.member_multiset [lemma, in BioFLL.LL.Multisets]
MultisetList.member_list_multiset [lemma, in BioFLL.LL.Multisets]
MultisetList.member_notempty [lemma, in BioFLL.LL.Multisets]
MultisetList.member_dec [lemma, in BioFLL.LL.Multisets]
MultisetList.member_ins_ins_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.member_meq_union [lemma, in BioFLL.LL.Multisets]
MultisetList.member_union [lemma, in BioFLL.LL.Multisets]
MultisetList.member_diff_member [lemma, in BioFLL.LL.Multisets]
MultisetList.member_insert [lemma, in BioFLL.LL.Multisets]
MultisetList.member_insert_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.member_insert_app [lemma, in BioFLL.LL.Multisets]
MultisetList.member_union_r [lemma, in BioFLL.LL.Multisets]
MultisetList.member_union_l [lemma, in BioFLL.LL.Multisets]
MultisetList.member_singleton [lemma, in BioFLL.LL.Multisets]
MultisetList.member_morph [instance, in BioFLL.LL.Multisets]
MultisetList.mem_step_not [lemma, in BioFLL.LL.Multisets]
MultisetList.mem_step [lemma, in BioFLL.LL.Multisets]
MultisetList.mem_memrem [lemma, in BioFLL.LL.Multisets]
MultisetList.meq [definition, in BioFLL.LL.Multisets]
MultisetList.meq_eq_s [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_swap' [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_cons_append [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_cons_In [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_In_In [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_swap_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_swap [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_skip [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_congr [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_remove_elem_right [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_diff_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_insert_remove [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_remove [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_remove_insert [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_ins_rem [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_ins_ins_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_meq_union [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_union_meq2 [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_union_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_cons_app [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_Equivalence [instance, in BioFLL.LL.Multisets]
MultisetList.meq_trans [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_sym [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_refl [lemma, in BioFLL.LL.Multisets]
MultisetList.meq_equivalence [section, in BioFLL.LL.Multisets]
MultisetList.meq_multeq [lemma, in BioFLL.LL.Multisets]
MultisetList.MulSingleton [lemma, in BioFLL.LL.Multisets]
MultisetList.mult [definition, in BioFLL.LL.Multisets]
MultisetList.multeq_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.multFalse [lemma, in BioFLL.LL.Multisets]
MultisetList.Multiset [section, in BioFLL.LL.Multisets]
MultisetList.Multiset [definition, in BioFLL.LL.Multisets]
MultisetList.multiset_twist2 [lemma, in BioFLL.LL.Multisets]
MultisetList.multiset_twist1 [lemma, in BioFLL.LL.Multisets]
MultisetList.multiset_meq_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.multiset_meq_non_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.Multiset2_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.mult_insert [lemma, in BioFLL.LL.Multisets]
MultisetList.mult_morph [instance, in BioFLL.LL.Multisets]
MultisetList.mult_remove_not_in [lemma, in BioFLL.LL.Multisets]
MultisetList.mult_remove_in [lemma, in BioFLL.LL.Multisets]
MultisetList.mult_eqA_compat [lemma, in BioFLL.LL.Multisets]
MultisetList.my_p [lemma, in BioFLL.LL.Multisets]
MultisetList.nil_contradiction [lemma, in BioFLL.LL.Multisets]
MultisetList.nil_rem [lemma, in BioFLL.LL.Multisets]
MultisetList.notempty_member [lemma, in BioFLL.LL.Multisets]
MultisetList.notInMul [lemma, in BioFLL.LL.Multisets]
MultisetList.not_eq_in [lemma, in BioFLL.LL.Multisets]
MultisetList.not_eq_zero [lemma, in BioFLL.LL.Multisets]
MultisetList.not_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.pair_app [lemma, in BioFLL.LL.Multisets]
MultisetList.Permutation_meq [lemma, in BioFLL.LL.Multisets]
MultisetList.permut_remove_hd [lemma, in BioFLL.LL.Multisets]
MultisetList.perm_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.perm_cons_single [lemma, in BioFLL.LL.Multisets]
MultisetList.principal [lemma, in BioFLL.LL.Multisets]
MultisetList.rem [definition, in BioFLL.LL.Multisets]
MultisetList.removeAll [definition, in BioFLL.LL.Multisets]
MultisetList.removeElem [definition, in BioFLL.LL.Multisets]
MultisetList.removeElem_length_in [lemma, in BioFLL.LL.Multisets]
MultisetList.remove_in_not [lemma, in BioFLL.LL.Multisets]
MultisetList.remove_union [lemma, in BioFLL.LL.Multisets]
MultisetList.remove_morph [instance, in BioFLL.LL.Multisets]
MultisetList.remove_perm_single' [lemma, in BioFLL.LL.Multisets]
MultisetList.remove_perm_single [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_not_abM [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_perm_not [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_skip [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_nil [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_to_union_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_to_union_app [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_aM_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_not_abM_app [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_abM_app [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_aM_app [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_aM [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_not_ab [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_ab [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_a [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_to_union [lemma, in BioFLL.LL.Multisets]
MultisetList.rem_morph [instance, in BioFLL.LL.Multisets]
MultisetList.rem_to_diff [lemma, in BioFLL.LL.Multisets]
MultisetList.resolvers [lemma, in BioFLL.LL.Multisets]
MultisetList.resolvers2 [lemma, in BioFLL.LL.Multisets]
MultisetList.resolvers3 [lemma, in BioFLL.LL.Multisets]
MultisetList.right_union [lemma, in BioFLL.LL.Multisets]
MultisetList.seconda [lemma, in BioFLL.LL.Multisets]
MultisetList.seconda_pri' [lemma, in BioFLL.LL.Multisets]
MultisetList.seconda_sec' [lemma, in BioFLL.LL.Multisets]
MultisetList.seconda_pri [lemma, in BioFLL.LL.Multisets]
MultisetList.seconda_sec [lemma, in BioFLL.LL.Multisets]
MultisetList.se_i [lemma, in BioFLL.LL.Multisets]
MultisetList.se_i2 [lemma, in BioFLL.LL.Multisets]
MultisetList.se_i3 [lemma, in BioFLL.LL.Multisets]
MultisetList.singleton [definition, in BioFLL.LL.Multisets]
MultisetList.singleton_notempty [lemma, in BioFLL.LL.Multisets]
MultisetList.singleton_member [lemma, in BioFLL.LL.Multisets]
MultisetList.singleton_mult_notin [lemma, in BioFLL.LL.Multisets]
MultisetList.singleton_mult_in [lemma, in BioFLL.LL.Multisets]
MultisetList.solsls [lemma, in BioFLL.LL.Multisets]
MultisetList.solsls2 [lemma, in BioFLL.LL.Multisets]
MultisetList.treesort_twist2 [lemma, in BioFLL.LL.Multisets]
MultisetList.treesort_twist1 [lemma, in BioFLL.LL.Multisets]
MultisetList.union [definition, in BioFLL.LL.Multisets]
MultisetList.union_middle [lemma, in BioFLL.LL.Multisets]
MultisetList.union_assoc_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.union_rotate_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.union_perm_left'' [lemma, in BioFLL.LL.Multisets]
MultisetList.union_perm_left' [lemma, in BioFLL.LL.Multisets]
MultisetList.union_perm_left [lemma, in BioFLL.LL.Multisets]
MultisetList.union_reverse [lemma, in BioFLL.LL.Multisets]
MultisetList.union_rotate [lemma, in BioFLL.LL.Multisets]
MultisetList.union_right [lemma, in BioFLL.LL.Multisets]
MultisetList.union_left [lemma, in BioFLL.LL.Multisets]
MultisetList.union_mult_step_eq [lemma, in BioFLL.LL.Multisets]
MultisetList.union_notempty [lemma, in BioFLL.LL.Multisets]
MultisetList.union_isempty [lemma, in BioFLL.LL.Multisets]
MultisetList.union_empty [lemma, in BioFLL.LL.Multisets]
MultisetList.union_perm [lemma, in BioFLL.LL.Multisets]
MultisetList.union_assoc [lemma, in BioFLL.LL.Multisets]
MultisetList.union_comm_cons [lemma, in BioFLL.LL.Multisets]
MultisetList.union_comm [lemma, in BioFLL.LL.Multisets]
MultisetList.union_morph' [instance, in BioFLL.LL.Multisets]
MultisetList.union_morph [instance, in BioFLL.LL.Multisets]
MultisetList.union_mult2 [lemma, in BioFLL.LL.Multisets]
MultisetList.union_mult [lemma, in BioFLL.LL.Multisets]
_ € _ [notation, in BioFLL.LL.Multisets]
_ # _ [notation, in BioFLL.LL.Multisets]
_ / _ [notation, in BioFLL.LL.Multisets]
_ <>mul _ [notation, in BioFLL.LL.Multisets]
_ =mul= _ [notation, in BioFLL.LL.Multisets]
Multisets [library]

N

NatSet [module, in BioFLL.LL.Eqset]
NatSet.A [definition, in BioFLL.LL.Eqset]
NatSet.eqA_dec [definition, in BioFLL.LL.Eqset]
NatSet.isPositive [definition, in BioFLL.LL.Eqset]
NONE [definition, in BioFLL.Definitions]

P

plusOne [inductive, in BioFLL.Definitions]
plus_le_reg_r [lemma, in BioFLL.LL.Eqset]
po_epmese [constructor, in BioFLL.Definitions]
po_epcdme2 [constructor, in BioFLL.Definitions]
po_epcdme1 [constructor, in BioFLL.Definitions]
po_epcd2 [constructor, in BioFLL.Definitions]
po_epcd1 [constructor, in BioFLL.Definitions]
po_ep1 [constructor, in BioFLL.Definitions]
po_ne [constructor, in BioFLL.Definitions]
po_nt [constructor, in BioFLL.Definitions]
Property1 [lemma, in BioFLL.ReachabilityProperties]
Property2 [lemma, in BioFLL.ReachabilityProperties]
Property3_Seq2 [lemma, in BioFLL.ReachabilityProperties]
Property3_Seq1 [lemma, in BioFLL.ReachabilityProperties]
Property4 [lemma, in BioFLL.MetaLevelProperties]
Property5 [lemma, in BioFLL.MetaLevelProperties]

R

ReachabilityProperties [library]

S

seeded [definition, in BioFLL.Definitions]
SequentCalculi [library]
SequentCalculiBasicTheory [library]
SLL [module, in BioFLL.Definitions]
SqBasic [module, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.AdequacyTri1 [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Height_leq [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.InitAtom [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.InitAtom' [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Init1 [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Init2 [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Sys [module, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TopDown [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TriExchange [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TriExchangeh [lemma, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.trih_morph' [instance, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.trih_morphh [instance, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.tri_morph' [instance, in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.tri_morph [instance, in BioFLL.LL.SequentCalculiBasicTheory]
SqSystems [module, in BioFLL.LL.SequentCalculi]
SqSystems.Arrow [inductive, in BioFLL.LL.SequentCalculi]
SqSystems.Arrow_eq_dec [lemma, in BioFLL.LL.SequentCalculi]
SqSystems.Arrow2LL [definition, in BioFLL.LL.SequentCalculi]
SqSystems.DW [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.SxLL [module, in BioFLL.LL.SequentCalculi]
SqSystems.trih_fx [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_ex [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_dec2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_dec1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_store [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_quest [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_with [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_par [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_bot [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_top [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_rel [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_bang [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_plus2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_plus1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_tensor [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_one [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_init2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.trih_init1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.TriSystem [inductive, in BioFLL.LL.SequentCalculi]
SqSystems.TriSystemh [inductive, in BioFLL.LL.SequentCalculi]
SqSystems.tri_fx [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_ex [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_dec2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_dec1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_store [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_quest [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_with [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_par [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_bot [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_top [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_rel [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_bang [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_plus2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_plus1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_tensor [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_one [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_init2 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.tri_init1 [constructor, in BioFLL.LL.SequentCalculi]
SqSystems.UP [constructor, in BioFLL.LL.SequentCalculi]
_ |-F- _ ; _ ; _ [notation, in BioFLL.LL.SequentCalculi]
|-F- _ ; _ ; _ [notation, in BioFLL.LL.SequentCalculi]
strind_hyp [lemma, in BioFLL.LL.StrongInduction]
strongind [lemma, in BioFLL.LL.StrongInduction]
StrongIndPrinciple [section, in BioFLL.LL.StrongInduction]
StrongIndPrinciple.P [variable, in BioFLL.LL.StrongInduction]
StrongIndPrinciple.Pn [variable, in BioFLL.LL.StrongInduction]
StrongIndPrinciple.P0 [variable, in BioFLL.LL.StrongInduction]
StrongInduction [library]
Syntax [library]
Syntax_LL.PosFIsNegAAsync [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegative [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NegativePositiveAtomNeg [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegativeAtomNeg [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegativeAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsIsPosRelease [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsyncRelease [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PosFNegAtomPorOrNegAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronousPosAtoms' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtomNotAssync [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelZero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelOne [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelEx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelBang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelPlus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotRelTensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeFx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeEx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeQuest [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeBang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePlus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeWith [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePar [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeTensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeTop [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeZero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeBot [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeOne [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAForall [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAExists [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAQuest [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPABang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAWith [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAPlus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAPar [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPATensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAZero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPAOne [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPABot [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotPATop [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncEx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncBang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncPlus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncTensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncZero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncOne [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncAtom' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PosOrNegAtomAsync [lemma, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePosOrNegAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NegPosAtomContradiction [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronousPosAtoms [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ApropPosNegAtom' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ApropPosNegAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PosFormulaPosOrNegAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PosFormula [definition, in BioFLL.LL.Syntax]
Syntax_LL.PFExists [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PFBang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PFPlus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PFTensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PFOne [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PFZero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.posFormula [inductive, in BioFLL.LL.Syntax]
Syntax_LL.PosOrNegAtom [definition, in BioFLL.LL.Syntax]
Syntax_LL.PPExists [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPBang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPPlus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPTensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPOne [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPZero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPAtom1' [constructor, in BioFLL.LL.Syntax]
Syntax_LL.PPAtom1 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.posOrNegAtom [inductive, in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqNeg [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousEquiv [lemma, in BioFLL.LL.Syntax]
Syntax_LL.NAExists [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NABang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NAPlus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NATensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NAOne [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NAZero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NAAtomN [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NAAtomP [constructor, in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronous [inductive, in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtomRelease [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Release [definition, in BioFLL.LL.Syntax]
Syntax_LL.RelForall [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelQuest [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelWith [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelPar [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelBot [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelTop [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelNA1' [constructor, in BioFLL.LL.Syntax]
Syntax_LL.RelNA1 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.release [inductive, in BioFLL.LL.Syntax]
Syntax_LL.NegPosAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousFlexpPos [lemma, in BioFLL.LL.Syntax]
Syntax_LL.lexpPos_lexpPos' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.lexpPosUnion_inv [lemma, in BioFLL.LL.Syntax]
Syntax_LL.lexpPosUnion [lemma, in BioFLL.LL.Syntax]
Syntax_LL.l_cos [constructor, in BioFLL.LL.Syntax]
Syntax_LL.l_sin [constructor, in BioFLL.LL.Syntax]
Syntax_LL.l_nil [constructor, in BioFLL.LL.Syntax]
Syntax_LL.LexpPos' [inductive, in BioFLL.LL.Syntax]
Syntax_LL.PosBool [lemma, in BioFLL.LL.Syntax]
Syntax_LL.BlexpPos [definition, in BioFLL.LL.Syntax]
Syntax_LL.LexpPos [definition, in BioFLL.LL.Syntax]
Syntax_LL.WeightFE [lemma, in BioFLL.LL.Syntax]
Syntax_LL.WeightEF [lemma, in BioFLL.LL.Syntax]
Syntax_LL.SubsDual' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.SubsDual [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Flatten_dual [lemma, in BioFLL.LL.Syntax]
Syntax_LL.subs_weight' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.subs_weight_weak' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.subs_weight [lemma, in BioFLL.LL.Syntax]
Syntax_LL.subs_weight_weak [lemma, in BioFLL.LL.Syntax]
Syntax_LL.FlattenPerp [lemma, in BioFLL.LL.Syntax]
Syntax_LL.FlattenAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenFun' [lemma, in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenFun [lemma, in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenG [lemma, in BioFLL.LL.Syntax]
Syntax_LL.WeightLeq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.L_weightApp [lemma, in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0LF [lemma, in BioFLL.LL.Syntax]
Syntax_LL.L_weight [definition, in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0F [lemma, in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Exp_weight [definition, in BioFLL.LL.Syntax]
Syntax_LL.exp_weight [definition, in BioFLL.LL.Syntax]
Syntax_LL.IsPAP' [constructor, in BioFLL.LL.Syntax]
Syntax_LL.IsPAP [constructor, in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtom [inductive, in BioFLL.LL.Syntax]
Syntax_LL.IsNAP' [constructor, in BioFLL.LL.Syntax]
Syntax_LL.IsNAP [constructor, in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeAtom [inductive, in BioFLL.LL.Syntax]
Syntax_LL.AsyncEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqR [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqL [lemma, in BioFLL.LL.Syntax]
Syntax_LL.aForall [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aQuest [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aWith [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aPar [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aBot [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aTop [constructor, in BioFLL.LL.Syntax]
Syntax_LL.Asynchronous [inductive, in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousF [definition, in BioFLL.LL.Syntax]
Syntax_LL.asynchronousF [definition, in BioFLL.LL.Syntax]
Syntax_LL.Polarities [section, in BioFLL.LL.Syntax]
Syntax_LL.subs_uptoAtomsL [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ax_lexp_uptoAtoms [axiom, in BioFLL.LL.Syntax]
Syntax_LL.ax_subs_uptoAtoms [axiom, in BioFLL.LL.Syntax]
Syntax_LL.eq_cons [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_nil [constructor, in BioFLL.LL.Syntax]
Syntax_LL.EqualUptoAtomsL [inductive, in BioFLL.LL.Syntax]
Syntax_LL.eq_fx [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_ex [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_quest [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_bang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_with [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_plus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_par [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_tensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_one [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_zero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_bot [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_top [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_perp [constructor, in BioFLL.LL.Syntax]
Syntax_LL.eq_atom [constructor, in BioFLL.LL.Syntax]
Syntax_LL.EqualUptoAtoms [inductive, in BioFLL.LL.Syntax]
Syntax_LL.xva_ap [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xVariantA [inductive, in BioFLL.LL.Syntax]
Syntax_LL.xvlt_cond [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xvlt_nil [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xVariantLT [inductive, in BioFLL.LL.Syntax]
Syntax_LL.xvt_fc2 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xvt_fc1 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xvt_cte [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xvt_var [constructor, in BioFLL.LL.Syntax]
Syntax_LL.xVariantT [inductive, in BioFLL.LL.Syntax]
Syntax_LL.EqUpTo.T' [variable, in BioFLL.LL.Syntax]
Syntax_LL.EqUpTo.T [variable, in BioFLL.LL.Syntax]
Syntax_LL.EqUpTo [section, in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual_plus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual [lemma, in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual_unit [lemma, in BioFLL.LL.Syntax]
Syntax_LL.wt_eq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.wt_trans [lemma, in BioFLL.LL.Syntax]
Syntax_LL.wt_symm [lemma, in BioFLL.LL.Syntax]
Syntax_LL.wt_refl [lemma, in BioFLL.LL.Syntax]
Syntax_LL.eq_wt [definition, in BioFLL.LL.Syntax]
Syntax_LL.WeightDestruct0 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Lexp_weight [definition, in BioFLL.LL.Syntax]
Syntax_LL.lexp_weight [definition, in BioFLL.LL.Syntax]
Syntax_LL.Measures [section, in BioFLL.LL.Syntax]
Syntax_LL.EqFC2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqFC1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqCte [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqAP [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqFx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqEx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqQuest [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqBang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqWith [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqPlus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqPar [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqTensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqZero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqOne [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqBot [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqTop [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqPerp [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqAtom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.APInvL [lemma, in BioFLL.LL.Syntax]
Syntax_LL.APInv [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Terms_fc1_fc2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Terms_cte_fc2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Terms_cte_fc1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.F2Eqt2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.F2Eqt1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.F2Eqn [lemma, in BioFLL.LL.Syntax]
Syntax_LL.F1Eqt [lemma, in BioFLL.LL.Syntax]
Syntax_LL.F1Eqn [lemma, in BioFLL.LL.Syntax]
Syntax_LL.CteEqt [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ExEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.FxEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.QuestEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.BangEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PlusEq2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PlusEq1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.TensorEq2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.TensorEq1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.WithEq2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.WithEq1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ParEq2 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ParEq1 [lemma, in BioFLL.LL.Syntax]
Syntax_LL.PerpEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AtomEq [lemma, in BioFLL.LL.Syntax]
Syntax_LL.EqualityFormulas [section, in BioFLL.LL.Syntax]
Syntax_LL.SubstL [definition, in BioFLL.LL.Syntax]
Syntax_LL.Subst [definition, in BioFLL.LL.Syntax]
Syntax_LL.flatten [definition, in BioFLL.LL.Syntax]
Syntax_LL.flattenT [definition, in BioFLL.LL.Syntax]
Syntax_LL.Substitution.T [variable, in BioFLL.LL.Syntax]
Syntax_LL.Substitution [section, in BioFLL.LL.Syntax]
Syntax_LL.Ng_involutive [lemma, in BioFLL.LL.Syntax]
Syntax_LL.Neg2pos [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AtomPos [lemma, in BioFLL.LL.Syntax]
Syntax_LL.AtomNeg [lemma, in BioFLL.LL.Syntax]
Syntax_LL.ex_fx [lemma, in BioFLL.LL.Syntax]
Syntax_LL.fx_ex [lemma, in BioFLL.LL.Syntax]
Syntax_LL.quest_bang [lemma, in BioFLL.LL.Syntax]
Syntax_LL.bang_quest [lemma, in BioFLL.LL.Syntax]
Syntax_LL.plus_with [lemma, in BioFLL.LL.Syntax]
Syntax_LL.with_plus [lemma, in BioFLL.LL.Syntax]
Syntax_LL.par_tensor [lemma, in BioFLL.LL.Syntax]
Syntax_LL.tensor_par [lemma, in BioFLL.LL.Syntax]
Syntax_LL.perp_atom [lemma, in BioFLL.LL.Syntax]
Syntax_LL.atom_perp [lemma, in BioFLL.LL.Syntax]
Syntax_LL.zero_top [lemma, in BioFLL.LL.Syntax]
Syntax_LL.top_zero [lemma, in BioFLL.LL.Syntax]
Syntax_LL.bot_one [lemma, in BioFLL.LL.Syntax]
Syntax_LL.one_bot [lemma, in BioFLL.LL.Syntax]
_ -o _ [notation, in BioFLL.LL.Syntax]
_ ° [notation, in BioFLL.LL.Syntax]
E{ _ } [notation, in BioFLL.LL.Syntax]
F{ _ } [notation, in BioFLL.LL.Syntax]
_ ⁻ [notation, in BioFLL.LL.Syntax]
_ ⁺ [notation, in BioFLL.LL.Syntax]
? _ [notation, in BioFLL.LL.Syntax]
! _ [notation, in BioFLL.LL.Syntax]
_ & _ [notation, in BioFLL.LL.Syntax]
_ ⊕ _ [notation, in BioFLL.LL.Syntax]
_ $ _ [notation, in BioFLL.LL.Syntax]
_ ** _ [notation, in BioFLL.LL.Syntax]
⊤ [notation, in BioFLL.LL.Syntax]
⊥ [notation, in BioFLL.LL.Syntax]
Syntax_LL.LLNotation [module, in BioFLL.LL.Syntax]
Syntax_LL.Dual_LExp [definition, in BioFLL.LL.Syntax]
Syntax_LL.Imp [definition, in BioFLL.LL.Syntax]
Syntax_LL.imp [definition, in BioFLL.LL.Syntax]
Syntax_LL.ng_involutive [lemma, in BioFLL.LL.Syntax]
Syntax_LL.dual_LExp [definition, in BioFLL.LL.Syntax]
Syntax_LL.Dualities.T [variable, in BioFLL.LL.Syntax]
Syntax_LL.Dualities [section, in BioFLL.LL.Syntax]
Syntax_LL.not_eqLExp_sym [lemma, in BioFLL.LL.Syntax]
Syntax_LL.FEqDec [axiom, in BioFLL.LL.Syntax]
Syntax_LL.ax_closed [axiom, in BioFLL.LL.Syntax]
Syntax_LL.ax_closedA [axiom, in BioFLL.LL.Syntax]
Syntax_LL.ax_closedT [axiom, in BioFLL.LL.Syntax]
Syntax_LL.cl_fx [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_ex [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_quest [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_bang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_with [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_plus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_par [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_tensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_top [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_zero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_bot [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_one [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_perp [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_atom [constructor, in BioFLL.LL.Syntax]
Syntax_LL.Closed [inductive, in BioFLL.LL.Syntax]
Syntax_LL.cl_ap [constructor, in BioFLL.LL.Syntax]
Syntax_LL.ClosedA [inductive, in BioFLL.LL.Syntax]
Syntax_LL.cl_fc2 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_fc1 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cl_cte [constructor, in BioFLL.LL.Syntax]
Syntax_LL.ClosedT [inductive, in BioFLL.LL.Syntax]
Syntax_LL.Fx [definition, in BioFLL.LL.Syntax]
Syntax_LL.Ex [definition, in BioFLL.LL.Syntax]
Syntax_LL.Quest [definition, in BioFLL.LL.Syntax]
Syntax_LL.Bang [definition, in BioFLL.LL.Syntax]
Syntax_LL.With [definition, in BioFLL.LL.Syntax]
Syntax_LL.Plus [definition, in BioFLL.LL.Syntax]
Syntax_LL.Par [definition, in BioFLL.LL.Syntax]
Syntax_LL.Tensor [definition, in BioFLL.LL.Syntax]
Syntax_LL.Zero [definition, in BioFLL.LL.Syntax]
Syntax_LL.One [definition, in BioFLL.LL.Syntax]
Syntax_LL.Bot [definition, in BioFLL.LL.Syntax]
Syntax_LL.Top [definition, in BioFLL.LL.Syntax]
Syntax_LL.Perp [definition, in BioFLL.LL.Syntax]
Syntax_LL.Atom [definition, in BioFLL.LL.Syntax]
Syntax_LL.AP [definition, in BioFLL.LL.Syntax]
Syntax_LL.FC2 [definition, in BioFLL.LL.Syntax]
Syntax_LL.FC1 [definition, in BioFLL.LL.Syntax]
Syntax_LL.Cte [definition, in BioFLL.LL.Syntax]
Syntax_LL.SubsL [definition, in BioFLL.LL.Syntax]
Syntax_LL.Subs [definition, in BioFLL.LL.Syntax]
Syntax_LL.Lexp [definition, in BioFLL.LL.Syntax]
Syntax_LL.AProp [definition, in BioFLL.LL.Syntax]
Syntax_LL.LTerm [definition, in BioFLL.LL.Syntax]
Syntax_LL.Term [definition, in BioFLL.LL.Syntax]
Syntax_LL.fx [constructor, in BioFLL.LL.Syntax]
Syntax_LL.ex [constructor, in BioFLL.LL.Syntax]
Syntax_LL.quest [constructor, in BioFLL.LL.Syntax]
Syntax_LL.bang [constructor, in BioFLL.LL.Syntax]
Syntax_LL.witH [constructor, in BioFLL.LL.Syntax]
Syntax_LL.plus [constructor, in BioFLL.LL.Syntax]
Syntax_LL.par [constructor, in BioFLL.LL.Syntax]
Syntax_LL.tensor [constructor, in BioFLL.LL.Syntax]
Syntax_LL.one [constructor, in BioFLL.LL.Syntax]
Syntax_LL.zero [constructor, in BioFLL.LL.Syntax]
Syntax_LL.bot [constructor, in BioFLL.LL.Syntax]
Syntax_LL.top [constructor, in BioFLL.LL.Syntax]
Syntax_LL.perp [constructor, in BioFLL.LL.Syntax]
Syntax_LL.atom [constructor, in BioFLL.LL.Syntax]
Syntax_LL.lexp [inductive, in BioFLL.LL.Syntax]
Syntax_LL.ap [constructor, in BioFLL.LL.Syntax]
Syntax_LL.aprop [inductive, in BioFLL.LL.Syntax]
Syntax_LL.fc2 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.fc1 [constructor, in BioFLL.LL.Syntax]
Syntax_LL.cte [constructor, in BioFLL.LL.Syntax]
Syntax_LL.var [constructor, in BioFLL.LL.Syntax]
Syntax_LL.term [inductive, in BioFLL.LL.Syntax]
Syntax_LL.Sec_lExp.T [variable, in BioFLL.LL.Syntax]
Syntax_LL.Sec_lExp [section, in BioFLL.LL.Syntax]
Syntax_LL [module, in BioFLL.LL.Syntax]

T

TG [definition, in BioFLL.Definitions]
TGFbeta [definition, in BioFLL.Definitions]
Theory [definition, in BioFLL.Definitions]
tri_dec2A [lemma, in BioFLL.Utils]

U

Utils [library]

other

_ s+ _ [notation, in BioFLL.Definitions]
AX{ _ } [notation, in BioFLL.Definitions]
A{ _ } [notation, in BioFLL.Definitions]
CF{ _ ; _ ; _ ; _ } [notation, in BioFLL.Definitions]
CX{ _ ; _ ; _ ; _ } [notation, in BioFLL.Definitions]
C{ _ ; _ ; _ ; _ } [notation, in BioFLL.Definitions]
DX{ _ , _ } [notation, in BioFLL.Definitions]
SX{ _ } [notation, in BioFLL.Definitions]
S{ _ } [notation, in BioFLL.Definitions]
Tn{ _ } [notation, in BioFLL.Definitions]
TX{ _ } [notation, in BioFLL.Definitions]
T{ _ } [notation, in BioFLL.Definitions]

Notation Index

M

_ € _ [in BioFLL.LL.Multisets]
_ # _ [in BioFLL.LL.Multisets]
_ / _ [in BioFLL.LL.Multisets]
_ <>mul _ [in BioFLL.LL.Multisets]
_ =mul= _ [in BioFLL.LL.Multisets]

S

_ |-F- _ ; _ ; _ [in BioFLL.LL.SequentCalculi]
|-F- _ ; _ ; _ [in BioFLL.LL.SequentCalculi]
_ -o _ [in BioFLL.LL.Syntax]
_ ° [in BioFLL.LL.Syntax]
E{ _ } [in BioFLL.LL.Syntax]
F{ _ } [in BioFLL.LL.Syntax]
_ ⁻ [in BioFLL.LL.Syntax]
_ ⁺ [in BioFLL.LL.Syntax]
? _ [in BioFLL.LL.Syntax]
! _ [in BioFLL.LL.Syntax]
_ & _ [in BioFLL.LL.Syntax]
_ ⊕ _ [in BioFLL.LL.Syntax]
_ $ _ [in BioFLL.LL.Syntax]
_ ** _ [in BioFLL.LL.Syntax]
⊤ [in BioFLL.LL.Syntax]
⊥ [in BioFLL.LL.Syntax]

other

_ s+ _ [in BioFLL.Definitions]
AX{ _ } [in BioFLL.Definitions]
A{ _ } [in BioFLL.Definitions]
CF{ _ ; _ ; _ ; _ } [in BioFLL.Definitions]
CX{ _ ; _ ; _ ; _ } [in BioFLL.Definitions]
C{ _ ; _ ; _ ; _ } [in BioFLL.Definitions]
DX{ _ , _ } [in BioFLL.Definitions]
SX{ _ } [in BioFLL.Definitions]
S{ _ } [in BioFLL.Definitions]
Tn{ _ } [in BioFLL.Definitions]
TX{ _ } [in BioFLL.Definitions]
T{ _ } [in BioFLL.Definitions]

Module Index

E

Eqset [in BioFLL.LL.Eqset]
Eqset_dec_pol [in BioFLL.LL.Eqset]
Eqset_dec [in BioFLL.LL.Eqset]

F

FormulasLL [in BioFLL.LL.Syntax]
FormulasLL.lexp_eq [in BioFLL.LL.Syntax]
FormulasLL.MSetList [in BioFLL.LL.Syntax]
FormulasLL.Sy [in BioFLL.LL.Syntax]

M

MultisetList [in BioFLL.LL.Multisets]

N

NatSet [in BioFLL.LL.Eqset]

S

SLL [in BioFLL.Definitions]
SqBasic [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Sys [in BioFLL.LL.SequentCalculiBasicTheory]
SqSystems [in BioFLL.LL.SequentCalculi]
SqSystems.SxLL [in BioFLL.LL.SequentCalculi]
Syntax_LL.LLNotation [in BioFLL.LL.Syntax]
Syntax_LL [in BioFLL.LL.Syntax]

Variable Index

S

StrongIndPrinciple.P [in BioFLL.LL.StrongInduction]
StrongIndPrinciple.Pn [in BioFLL.LL.StrongInduction]
StrongIndPrinciple.P0 [in BioFLL.LL.StrongInduction]
Syntax_LL.EqUpTo.T' [in BioFLL.LL.Syntax]
Syntax_LL.EqUpTo.T [in BioFLL.LL.Syntax]
Syntax_LL.Substitution.T [in BioFLL.LL.Syntax]
Syntax_LL.Dualities.T [in BioFLL.LL.Syntax]
Syntax_LL.Sec_lExp.T [in BioFLL.LL.Syntax]

Library Index

D

E

Eqset

I

InversionTactics

M

MetaLevelProperties
Multisets

R

ReachabilityProperties

S

SequentCalculi
SequentCalculiBasicTheory
StrongInduction
Syntax

U

Utils

Lemma Index

A

AtomNotInTheory [in BioFLL.Utils]

E

EqC [in BioFLL.Utils]
EqL [in BioFLL.Utils]
EqT [in BioFLL.Utils]
EqTFC [in BioFLL.Utils]
ExTXT [in BioFLL.Utils]

F

FocusAtom [in BioFLL.InversionTactics]
FocusOnlyTheory [in BioFLL.Utils]
FocusonParAtom [in BioFLL.InversionTactics]
FocusTensorAtom [in BioFLL.InversionTactics]
FormulasLL.LexpPosConc [in BioFLL.LL.Syntax]
FormulasLL.LexpPosCons [in BioFLL.LL.Syntax]
FormulasLL.LexpPosOrNegAtomConc [in BioFLL.LL.Syntax]
FormulasLL.LPos1 [in BioFLL.LL.Syntax]
FormulasLL.LPos2 [in BioFLL.LL.Syntax]
FormulasLL.LPos3 [in BioFLL.LL.Syntax]

G

GtZero [in BioFLL.LL.Eqset]

I

InMeq [in BioFLL.Utils]
InvRuleTheory [in BioFLL.InversionTactics]
InvRuleTheoryAp [in BioFLL.InversionTactics]

M

MultisetList.aunion_comm [in BioFLL.LL.Multisets]
MultisetList.axPair [in BioFLL.LL.Multisets]
MultisetList.countIn_In [in BioFLL.LL.Multisets]
MultisetList.countIn_cons_neq [in BioFLL.LL.Multisets]
MultisetList.countIn_cons_eq [in BioFLL.LL.Multisets]
MultisetList.countIn_inv_nil [in BioFLL.LL.Multisets]
MultisetList.countIn_not_In [in BioFLL.LL.Multisets]
MultisetList.countIn_nil [in BioFLL.LL.Multisets]
MultisetList.DestructMSet [in BioFLL.LL.Multisets]
MultisetList.DestructMSet' [in BioFLL.LL.Multisets]
MultisetList.DestructMSet2 [in BioFLL.LL.Multisets]
MultisetList.DestructMSet2_aux [in BioFLL.LL.Multisets]
MultisetList.DestructMSet2' [in BioFLL.LL.Multisets]
MultisetList.DestructMulFalse [in BioFLL.LL.Multisets]
MultisetList.diff_MM_empty [in BioFLL.LL.Multisets]
MultisetList.diff_remove_both [in BioFLL.LL.Multisets]
MultisetList.diff_member_ly_rn [in BioFLL.LL.Multisets]
MultisetList.diff_mult [in BioFLL.LL.Multisets]
MultisetList.diff_mult_step_neq [in BioFLL.LL.Multisets]
MultisetList.diff_mult_step_eq [in BioFLL.LL.Multisets]
MultisetList.diff_perm [in BioFLL.LL.Multisets]
MultisetList.diff_perm_single [in BioFLL.LL.Multisets]
MultisetList.diff_mult_comp [in BioFLL.LL.Multisets]
MultisetList.diff_empty_r [in BioFLL.LL.Multisets]
MultisetList.diff_empty_l [in BioFLL.LL.Multisets]
MultisetList.EmptyMS [in BioFLL.LL.Multisets]
MultisetList.empty_decomp_dec [in BioFLL.LL.Multisets]
MultisetList.empty_dec [in BioFLL.LL.Multisets]
MultisetList.empty_mult [in BioFLL.LL.Multisets]
MultisetList.empty_empty [in BioFLL.LL.Multisets]
MultisetList.emp_mult [in BioFLL.LL.Multisets]
MultisetList.eq_then_meq [in BioFLL.LL.Multisets]
MultisetList.eq_step [in BioFLL.LL.Multisets]
MultisetList.insert_remove_noteq [in BioFLL.LL.Multisets]
MultisetList.insert_remove_eq [in BioFLL.LL.Multisets]
MultisetList.insert_meq [in BioFLL.LL.Multisets]
MultisetList.ins_meq_union [in BioFLL.LL.Multisets]
MultisetList.In_to_in [in BioFLL.LL.Multisets]
MultisetList.In_union_or' [in BioFLL.LL.Multisets]
MultisetList.In_union_or [in BioFLL.LL.Multisets]
MultisetList.in_countIn [in BioFLL.LL.Multisets]
MultisetList.lenghtList [in BioFLL.LL.Multisets]
MultisetList.member_due [in BioFLL.LL.Multisets]
MultisetList.member_unit [in BioFLL.LL.Multisets]
MultisetList.member_then_meq [in BioFLL.LL.Multisets]
MultisetList.member_then_eq [in BioFLL.LL.Multisets]
MultisetList.member_multiset [in BioFLL.LL.Multisets]
MultisetList.member_list_multiset [in BioFLL.LL.Multisets]
MultisetList.member_notempty [in BioFLL.LL.Multisets]
MultisetList.member_dec [in BioFLL.LL.Multisets]
MultisetList.member_ins_ins_meq [in BioFLL.LL.Multisets]
MultisetList.member_meq_union [in BioFLL.LL.Multisets]
MultisetList.member_union [in BioFLL.LL.Multisets]
MultisetList.member_diff_member [in BioFLL.LL.Multisets]
MultisetList.member_insert [in BioFLL.LL.Multisets]
MultisetList.member_insert_cons [in BioFLL.LL.Multisets]
MultisetList.member_insert_app [in BioFLL.LL.Multisets]
MultisetList.member_union_r [in BioFLL.LL.Multisets]
MultisetList.member_union_l [in BioFLL.LL.Multisets]
MultisetList.member_singleton [in BioFLL.LL.Multisets]
MultisetList.mem_step_not [in BioFLL.LL.Multisets]
MultisetList.mem_step [in BioFLL.LL.Multisets]
MultisetList.mem_memrem [in BioFLL.LL.Multisets]
MultisetList.meq_eq_s [in BioFLL.LL.Multisets]
MultisetList.meq_swap' [in BioFLL.LL.Multisets]
MultisetList.meq_cons_append [in BioFLL.LL.Multisets]
MultisetList.meq_cons_In [in BioFLL.LL.Multisets]
MultisetList.meq_In_In [in BioFLL.LL.Multisets]
MultisetList.meq_swap_cons [in BioFLL.LL.Multisets]
MultisetList.meq_swap [in BioFLL.LL.Multisets]
MultisetList.meq_skip [in BioFLL.LL.Multisets]
MultisetList.meq_congr [in BioFLL.LL.Multisets]
MultisetList.meq_remove_elem_right [in BioFLL.LL.Multisets]
MultisetList.meq_diff_meq [in BioFLL.LL.Multisets]
MultisetList.meq_cons [in BioFLL.LL.Multisets]
MultisetList.meq_insert_remove [in BioFLL.LL.Multisets]
MultisetList.meq_remove [in BioFLL.LL.Multisets]
MultisetList.meq_remove_insert [in BioFLL.LL.Multisets]
MultisetList.meq_ins_rem [in BioFLL.LL.Multisets]
MultisetList.meq_ins_ins_eq [in BioFLL.LL.Multisets]
MultisetList.meq_meq_union [in BioFLL.LL.Multisets]
MultisetList.meq_union_meq2 [in BioFLL.LL.Multisets]
MultisetList.meq_union_meq [in BioFLL.LL.Multisets]
MultisetList.meq_cons_app [in BioFLL.LL.Multisets]
MultisetList.meq_trans [in BioFLL.LL.Multisets]
MultisetList.meq_sym [in BioFLL.LL.Multisets]
MultisetList.meq_refl [in BioFLL.LL.Multisets]
MultisetList.meq_multeq [in BioFLL.LL.Multisets]
MultisetList.MulSingleton [in BioFLL.LL.Multisets]
MultisetList.multeq_meq [in BioFLL.LL.Multisets]
MultisetList.multFalse [in BioFLL.LL.Multisets]
MultisetList.multiset_twist2 [in BioFLL.LL.Multisets]
MultisetList.multiset_twist1 [in BioFLL.LL.Multisets]
MultisetList.multiset_meq_empty [in BioFLL.LL.Multisets]
MultisetList.multiset_meq_non_empty [in BioFLL.LL.Multisets]
MultisetList.Multiset2_empty [in BioFLL.LL.Multisets]
MultisetList.mult_insert [in BioFLL.LL.Multisets]
MultisetList.mult_remove_not_in [in BioFLL.LL.Multisets]
MultisetList.mult_remove_in [in BioFLL.LL.Multisets]
MultisetList.mult_eqA_compat [in BioFLL.LL.Multisets]
MultisetList.my_p [in BioFLL.LL.Multisets]
MultisetList.nil_contradiction [in BioFLL.LL.Multisets]
MultisetList.nil_rem [in BioFLL.LL.Multisets]
MultisetList.notempty_member [in BioFLL.LL.Multisets]
MultisetList.notInMul [in BioFLL.LL.Multisets]
MultisetList.not_eq_in [in BioFLL.LL.Multisets]
MultisetList.not_eq_zero [in BioFLL.LL.Multisets]
MultisetList.not_empty [in BioFLL.LL.Multisets]
MultisetList.pair_app [in BioFLL.LL.Multisets]
MultisetList.Permutation_meq [in BioFLL.LL.Multisets]
MultisetList.permut_remove_hd [in BioFLL.LL.Multisets]
MultisetList.perm_cons [in BioFLL.LL.Multisets]
MultisetList.perm_cons_single [in BioFLL.LL.Multisets]
MultisetList.principal [in BioFLL.LL.Multisets]
MultisetList.removeElem_length_in [in BioFLL.LL.Multisets]
MultisetList.remove_in_not [in BioFLL.LL.Multisets]
MultisetList.remove_union [in BioFLL.LL.Multisets]
MultisetList.remove_perm_single' [in BioFLL.LL.Multisets]
MultisetList.remove_perm_single [in BioFLL.LL.Multisets]
MultisetList.rem_not_abM [in BioFLL.LL.Multisets]
MultisetList.rem_perm_not [in BioFLL.LL.Multisets]
MultisetList.rem_skip [in BioFLL.LL.Multisets]
MultisetList.rem_nil [in BioFLL.LL.Multisets]
MultisetList.rem_to_union_cons [in BioFLL.LL.Multisets]
MultisetList.rem_to_union_app [in BioFLL.LL.Multisets]
MultisetList.rem_aM_cons [in BioFLL.LL.Multisets]
MultisetList.rem_not_abM_app [in BioFLL.LL.Multisets]
MultisetList.rem_abM_app [in BioFLL.LL.Multisets]
MultisetList.rem_aM_app [in BioFLL.LL.Multisets]
MultisetList.rem_aM [in BioFLL.LL.Multisets]
MultisetList.rem_not_ab [in BioFLL.LL.Multisets]
MultisetList.rem_ab [in BioFLL.LL.Multisets]
MultisetList.rem_a [in BioFLL.LL.Multisets]
MultisetList.rem_to_union [in BioFLL.LL.Multisets]
MultisetList.rem_to_diff [in BioFLL.LL.Multisets]
MultisetList.resolvers [in BioFLL.LL.Multisets]
MultisetList.resolvers2 [in BioFLL.LL.Multisets]
MultisetList.resolvers3 [in BioFLL.LL.Multisets]
MultisetList.right_union [in BioFLL.LL.Multisets]
MultisetList.seconda [in BioFLL.LL.Multisets]
MultisetList.seconda_pri' [in BioFLL.LL.Multisets]
MultisetList.seconda_sec' [in BioFLL.LL.Multisets]
MultisetList.seconda_pri [in BioFLL.LL.Multisets]
MultisetList.seconda_sec [in BioFLL.LL.Multisets]
MultisetList.se_i [in BioFLL.LL.Multisets]
MultisetList.se_i2 [in BioFLL.LL.Multisets]
MultisetList.se_i3 [in BioFLL.LL.Multisets]
MultisetList.singleton_notempty [in BioFLL.LL.Multisets]
MultisetList.singleton_member [in BioFLL.LL.Multisets]
MultisetList.singleton_mult_notin [in BioFLL.LL.Multisets]
MultisetList.singleton_mult_in [in BioFLL.LL.Multisets]
MultisetList.solsls [in BioFLL.LL.Multisets]
MultisetList.solsls2 [in BioFLL.LL.Multisets]
MultisetList.treesort_twist2 [in BioFLL.LL.Multisets]
MultisetList.treesort_twist1 [in BioFLL.LL.Multisets]
MultisetList.union_middle [in BioFLL.LL.Multisets]
MultisetList.union_assoc_cons [in BioFLL.LL.Multisets]
MultisetList.union_rotate_cons [in BioFLL.LL.Multisets]
MultisetList.union_perm_left'' [in BioFLL.LL.Multisets]
MultisetList.union_perm_left' [in BioFLL.LL.Multisets]
MultisetList.union_perm_left [in BioFLL.LL.Multisets]
MultisetList.union_reverse [in BioFLL.LL.Multisets]
MultisetList.union_rotate [in BioFLL.LL.Multisets]
MultisetList.union_right [in BioFLL.LL.Multisets]
MultisetList.union_left [in BioFLL.LL.Multisets]
MultisetList.union_mult_step_eq [in BioFLL.LL.Multisets]
MultisetList.union_notempty [in BioFLL.LL.Multisets]
MultisetList.union_isempty [in BioFLL.LL.Multisets]
MultisetList.union_empty [in BioFLL.LL.Multisets]
MultisetList.union_perm [in BioFLL.LL.Multisets]
MultisetList.union_assoc [in BioFLL.LL.Multisets]
MultisetList.union_comm_cons [in BioFLL.LL.Multisets]
MultisetList.union_comm [in BioFLL.LL.Multisets]
MultisetList.union_mult2 [in BioFLL.LL.Multisets]
MultisetList.union_mult [in BioFLL.LL.Multisets]

P

plus_le_reg_r [in BioFLL.LL.Eqset]
Property1 [in BioFLL.ReachabilityProperties]
Property2 [in BioFLL.ReachabilityProperties]
Property3_Seq2 [in BioFLL.ReachabilityProperties]
Property3_Seq1 [in BioFLL.ReachabilityProperties]
Property4 [in BioFLL.MetaLevelProperties]
Property5 [in BioFLL.MetaLevelProperties]

S

SqBasic.AdequacyTri1 [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Height_leq [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.InitAtom [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.InitAtom' [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Init1 [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.Init2 [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TopDown [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TriExchange [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.TriExchangeh [in BioFLL.LL.SequentCalculiBasicTheory]
SqSystems.Arrow_eq_dec [in BioFLL.LL.SequentCalculi]
strind_hyp [in BioFLL.LL.StrongInduction]
strongind [in BioFLL.LL.StrongInduction]
Syntax_LL.PosFIsNegAAsync [in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegative [in BioFLL.LL.Syntax]
Syntax_LL.NegativePositiveAtomNeg [in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegativeAtomNeg [in BioFLL.LL.Syntax]
Syntax_LL.PositiveNegativeAtom [in BioFLL.LL.Syntax]
Syntax_LL.AsIsPosRelease [in BioFLL.LL.Syntax]
Syntax_LL.AsyncRelease [in BioFLL.LL.Syntax]
Syntax_LL.PosFNegAtomPorOrNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronousPosAtoms' [in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtomNotAssync [in BioFLL.LL.Syntax]
Syntax_LL.NotRelZero [in BioFLL.LL.Syntax]
Syntax_LL.NotRelOne [in BioFLL.LL.Syntax]
Syntax_LL.NotRelEx [in BioFLL.LL.Syntax]
Syntax_LL.NotRelBang [in BioFLL.LL.Syntax]
Syntax_LL.NotRelPlus [in BioFLL.LL.Syntax]
Syntax_LL.NotRelTensor [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeFx [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeEx [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeQuest [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeBang [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePlus [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeWith [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePar [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeTensor [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeTop [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeZero [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeBot [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeOne [in BioFLL.LL.Syntax]
Syntax_LL.NotPAForall [in BioFLL.LL.Syntax]
Syntax_LL.NotPAExists [in BioFLL.LL.Syntax]
Syntax_LL.NotPAQuest [in BioFLL.LL.Syntax]
Syntax_LL.NotPABang [in BioFLL.LL.Syntax]
Syntax_LL.NotPAWith [in BioFLL.LL.Syntax]
Syntax_LL.NotPAPlus [in BioFLL.LL.Syntax]
Syntax_LL.NotPAPar [in BioFLL.LL.Syntax]
Syntax_LL.NotPATensor [in BioFLL.LL.Syntax]
Syntax_LL.NotPAZero [in BioFLL.LL.Syntax]
Syntax_LL.NotPAOne [in BioFLL.LL.Syntax]
Syntax_LL.NotPABot [in BioFLL.LL.Syntax]
Syntax_LL.NotPATop [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncEx [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncBang [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncPlus [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncTensor [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncZero [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncOne [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncAtom' [in BioFLL.LL.Syntax]
Syntax_LL.NotAsyncAtom [in BioFLL.LL.Syntax]
Syntax_LL.PosOrNegAtomAsync [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativePosOrNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.NegPosAtomContradiction [in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronousPosAtoms [in BioFLL.LL.Syntax]
Syntax_LL.ApropPosNegAtom' [in BioFLL.LL.Syntax]
Syntax_LL.ApropPosNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.PosFormulaPosOrNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqNeg [in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousEquiv [in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtomRelease [in BioFLL.LL.Syntax]
Syntax_LL.NegPosAtom [in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousFlexpPos [in BioFLL.LL.Syntax]
Syntax_LL.lexpPos_lexpPos' [in BioFLL.LL.Syntax]
Syntax_LL.lexpPosUnion_inv [in BioFLL.LL.Syntax]
Syntax_LL.lexpPosUnion [in BioFLL.LL.Syntax]
Syntax_LL.PosBool [in BioFLL.LL.Syntax]
Syntax_LL.WeightFE [in BioFLL.LL.Syntax]
Syntax_LL.WeightEF [in BioFLL.LL.Syntax]
Syntax_LL.SubsDual' [in BioFLL.LL.Syntax]
Syntax_LL.SubsDual [in BioFLL.LL.Syntax]
Syntax_LL.Flatten_dual [in BioFLL.LL.Syntax]
Syntax_LL.subs_weight' [in BioFLL.LL.Syntax]
Syntax_LL.subs_weight_weak' [in BioFLL.LL.Syntax]
Syntax_LL.subs_weight [in BioFLL.LL.Syntax]
Syntax_LL.subs_weight_weak [in BioFLL.LL.Syntax]
Syntax_LL.FlattenPerp [in BioFLL.LL.Syntax]
Syntax_LL.FlattenAtom [in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenFun' [in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenFun [in BioFLL.LL.Syntax]
Syntax_LL.TermFlattenG [in BioFLL.LL.Syntax]
Syntax_LL.WeightLeq [in BioFLL.LL.Syntax]
Syntax_LL.L_weightApp [in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0LF [in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0F [in BioFLL.LL.Syntax]
Syntax_LL.exp_weight0 [in BioFLL.LL.Syntax]
Syntax_LL.AsyncEq [in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqR [in BioFLL.LL.Syntax]
Syntax_LL.AsyncEqL [in BioFLL.LL.Syntax]
Syntax_LL.subs_uptoAtomsL [in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual_plus [in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual [in BioFLL.LL.Syntax]
Syntax_LL.lweight_dual_unit [in BioFLL.LL.Syntax]
Syntax_LL.wt_eq [in BioFLL.LL.Syntax]
Syntax_LL.wt_trans [in BioFLL.LL.Syntax]
Syntax_LL.wt_symm [in BioFLL.LL.Syntax]
Syntax_LL.wt_refl [in BioFLL.LL.Syntax]
Syntax_LL.WeightDestruct0 [in BioFLL.LL.Syntax]
Syntax_LL.EqFC2 [in BioFLL.LL.Syntax]
Syntax_LL.EqFC1 [in BioFLL.LL.Syntax]
Syntax_LL.EqCte [in BioFLL.LL.Syntax]
Syntax_LL.EqAP [in BioFLL.LL.Syntax]
Syntax_LL.EqFx [in BioFLL.LL.Syntax]
Syntax_LL.EqEx [in BioFLL.LL.Syntax]
Syntax_LL.EqQuest [in BioFLL.LL.Syntax]
Syntax_LL.EqBang [in BioFLL.LL.Syntax]
Syntax_LL.EqWith [in BioFLL.LL.Syntax]
Syntax_LL.EqPlus [in BioFLL.LL.Syntax]
Syntax_LL.EqPar [in BioFLL.LL.Syntax]
Syntax_LL.EqTensor [in BioFLL.LL.Syntax]
Syntax_LL.EqZero [in BioFLL.LL.Syntax]
Syntax_LL.EqOne [in BioFLL.LL.Syntax]
Syntax_LL.EqBot [in BioFLL.LL.Syntax]
Syntax_LL.EqTop [in BioFLL.LL.Syntax]
Syntax_LL.EqPerp [in BioFLL.LL.Syntax]
Syntax_LL.EqAtom [in BioFLL.LL.Syntax]
Syntax_LL.APInvL [in BioFLL.LL.Syntax]
Syntax_LL.APInv [in BioFLL.LL.Syntax]
Syntax_LL.Terms_fc1_fc2 [in BioFLL.LL.Syntax]
Syntax_LL.Terms_cte_fc2 [in BioFLL.LL.Syntax]
Syntax_LL.Terms_cte_fc1 [in BioFLL.LL.Syntax]
Syntax_LL.F2Eqt2 [in BioFLL.LL.Syntax]
Syntax_LL.F2Eqt1 [in BioFLL.LL.Syntax]
Syntax_LL.F2Eqn [in BioFLL.LL.Syntax]
Syntax_LL.F1Eqt [in BioFLL.LL.Syntax]
Syntax_LL.F1Eqn [in BioFLL.LL.Syntax]
Syntax_LL.CteEqt [in BioFLL.LL.Syntax]
Syntax_LL.ExEq [in BioFLL.LL.Syntax]
Syntax_LL.FxEq [in BioFLL.LL.Syntax]
Syntax_LL.QuestEq [in BioFLL.LL.Syntax]
Syntax_LL.BangEq [in BioFLL.LL.Syntax]
Syntax_LL.PlusEq2 [in BioFLL.LL.Syntax]
Syntax_LL.PlusEq1 [in BioFLL.LL.Syntax]
Syntax_LL.TensorEq2 [in BioFLL.LL.Syntax]
Syntax_LL.TensorEq1 [in BioFLL.LL.Syntax]
Syntax_LL.WithEq2 [in BioFLL.LL.Syntax]
Syntax_LL.WithEq1 [in BioFLL.LL.Syntax]
Syntax_LL.ParEq2 [in BioFLL.LL.Syntax]
Syntax_LL.ParEq1 [in BioFLL.LL.Syntax]
Syntax_LL.PerpEq [in BioFLL.LL.Syntax]
Syntax_LL.AtomEq [in BioFLL.LL.Syntax]
Syntax_LL.Ng_involutive [in BioFLL.LL.Syntax]
Syntax_LL.Neg2pos [in BioFLL.LL.Syntax]
Syntax_LL.AtomPos [in BioFLL.LL.Syntax]
Syntax_LL.AtomNeg [in BioFLL.LL.Syntax]
Syntax_LL.ex_fx [in BioFLL.LL.Syntax]
Syntax_LL.fx_ex [in BioFLL.LL.Syntax]
Syntax_LL.quest_bang [in BioFLL.LL.Syntax]
Syntax_LL.bang_quest [in BioFLL.LL.Syntax]
Syntax_LL.plus_with [in BioFLL.LL.Syntax]
Syntax_LL.with_plus [in BioFLL.LL.Syntax]
Syntax_LL.par_tensor [in BioFLL.LL.Syntax]
Syntax_LL.tensor_par [in BioFLL.LL.Syntax]
Syntax_LL.perp_atom [in BioFLL.LL.Syntax]
Syntax_LL.atom_perp [in BioFLL.LL.Syntax]
Syntax_LL.zero_top [in BioFLL.LL.Syntax]
Syntax_LL.top_zero [in BioFLL.LL.Syntax]
Syntax_LL.bot_one [in BioFLL.LL.Syntax]
Syntax_LL.one_bot [in BioFLL.LL.Syntax]
Syntax_LL.ng_involutive [in BioFLL.LL.Syntax]
Syntax_LL.not_eqLExp_sym [in BioFLL.LL.Syntax]

T

tri_dec2A [in BioFLL.Utils]

Axiom Index

E

Eqset_dec_pol.isPositive [in BioFLL.LL.Eqset]
Eqset_dec_pol.eqA_dec [in BioFLL.LL.Eqset]
Eqset_dec_pol.A [in BioFLL.LL.Eqset]
Eqset_dec.eqA_dec [in BioFLL.LL.Eqset]
Eqset_dec.A [in BioFLL.LL.Eqset]
Eqset.A [in BioFLL.LL.Eqset]

S

Syntax_LL.ax_lexp_uptoAtoms [in BioFLL.LL.Syntax]
Syntax_LL.ax_subs_uptoAtoms [in BioFLL.LL.Syntax]
Syntax_LL.FEqDec [in BioFLL.LL.Syntax]
Syntax_LL.ax_closed [in BioFLL.LL.Syntax]
Syntax_LL.ax_closedA [in BioFLL.LL.Syntax]
Syntax_LL.ax_closedT [in BioFLL.LL.Syntax]

Constructor Index

P

po_epmese [in BioFLL.Definitions]
po_epcdme2 [in BioFLL.Definitions]
po_epcdme1 [in BioFLL.Definitions]
po_epcd2 [in BioFLL.Definitions]
po_epcd1 [in BioFLL.Definitions]
po_ep1 [in BioFLL.Definitions]
po_ne [in BioFLL.Definitions]
po_nt [in BioFLL.Definitions]

S

SqSystems.DW [in BioFLL.LL.SequentCalculi]
SqSystems.trih_fx [in BioFLL.LL.SequentCalculi]
SqSystems.trih_ex [in BioFLL.LL.SequentCalculi]
SqSystems.trih_dec2 [in BioFLL.LL.SequentCalculi]
SqSystems.trih_dec1 [in BioFLL.LL.SequentCalculi]
SqSystems.trih_store [in BioFLL.LL.SequentCalculi]
SqSystems.trih_quest [in BioFLL.LL.SequentCalculi]
SqSystems.trih_with [in BioFLL.LL.SequentCalculi]
SqSystems.trih_par [in BioFLL.LL.SequentCalculi]
SqSystems.trih_bot [in BioFLL.LL.SequentCalculi]
SqSystems.trih_top [in BioFLL.LL.SequentCalculi]
SqSystems.trih_rel [in BioFLL.LL.SequentCalculi]
SqSystems.trih_bang [in BioFLL.LL.SequentCalculi]
SqSystems.trih_plus2 [in BioFLL.LL.SequentCalculi]
SqSystems.trih_plus1 [in BioFLL.LL.SequentCalculi]
SqSystems.trih_tensor [in BioFLL.LL.SequentCalculi]
SqSystems.trih_one [in BioFLL.LL.SequentCalculi]
SqSystems.trih_init2 [in BioFLL.LL.SequentCalculi]
SqSystems.trih_init1 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_fx [in BioFLL.LL.SequentCalculi]
SqSystems.tri_ex [in BioFLL.LL.SequentCalculi]
SqSystems.tri_dec2 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_dec1 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_store [in BioFLL.LL.SequentCalculi]
SqSystems.tri_quest [in BioFLL.LL.SequentCalculi]
SqSystems.tri_with [in BioFLL.LL.SequentCalculi]
SqSystems.tri_par [in BioFLL.LL.SequentCalculi]
SqSystems.tri_bot [in BioFLL.LL.SequentCalculi]
SqSystems.tri_top [in BioFLL.LL.SequentCalculi]
SqSystems.tri_rel [in BioFLL.LL.SequentCalculi]
SqSystems.tri_bang [in BioFLL.LL.SequentCalculi]
SqSystems.tri_plus2 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_plus1 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_tensor [in BioFLL.LL.SequentCalculi]
SqSystems.tri_one [in BioFLL.LL.SequentCalculi]
SqSystems.tri_init2 [in BioFLL.LL.SequentCalculi]
SqSystems.tri_init1 [in BioFLL.LL.SequentCalculi]
SqSystems.UP [in BioFLL.LL.SequentCalculi]
Syntax_LL.PFExists [in BioFLL.LL.Syntax]
Syntax_LL.PFBang [in BioFLL.LL.Syntax]
Syntax_LL.PFPlus [in BioFLL.LL.Syntax]
Syntax_LL.PFTensor [in BioFLL.LL.Syntax]
Syntax_LL.PFOne [in BioFLL.LL.Syntax]
Syntax_LL.PFZero [in BioFLL.LL.Syntax]
Syntax_LL.PPExists [in BioFLL.LL.Syntax]
Syntax_LL.PPBang [in BioFLL.LL.Syntax]
Syntax_LL.PPPlus [in BioFLL.LL.Syntax]
Syntax_LL.PPTensor [in BioFLL.LL.Syntax]
Syntax_LL.PPOne [in BioFLL.LL.Syntax]
Syntax_LL.PPZero [in BioFLL.LL.Syntax]
Syntax_LL.PPAtom1' [in BioFLL.LL.Syntax]
Syntax_LL.PPAtom1 [in BioFLL.LL.Syntax]
Syntax_LL.NAExists [in BioFLL.LL.Syntax]
Syntax_LL.NABang [in BioFLL.LL.Syntax]
Syntax_LL.NAPlus [in BioFLL.LL.Syntax]
Syntax_LL.NATensor [in BioFLL.LL.Syntax]
Syntax_LL.NAOne [in BioFLL.LL.Syntax]
Syntax_LL.NAZero [in BioFLL.LL.Syntax]
Syntax_LL.NAAtomN [in BioFLL.LL.Syntax]
Syntax_LL.NAAtomP [in BioFLL.LL.Syntax]
Syntax_LL.RelForall [in BioFLL.LL.Syntax]
Syntax_LL.RelQuest [in BioFLL.LL.Syntax]
Syntax_LL.RelWith [in BioFLL.LL.Syntax]
Syntax_LL.RelPar [in BioFLL.LL.Syntax]
Syntax_LL.RelBot [in BioFLL.LL.Syntax]
Syntax_LL.RelTop [in BioFLL.LL.Syntax]
Syntax_LL.RelNA1' [in BioFLL.LL.Syntax]
Syntax_LL.RelNA1 [in BioFLL.LL.Syntax]
Syntax_LL.l_cos [in BioFLL.LL.Syntax]
Syntax_LL.l_sin [in BioFLL.LL.Syntax]
Syntax_LL.l_nil [in BioFLL.LL.Syntax]
Syntax_LL.IsPAP' [in BioFLL.LL.Syntax]
Syntax_LL.IsPAP [in BioFLL.LL.Syntax]
Syntax_LL.IsNAP' [in BioFLL.LL.Syntax]
Syntax_LL.IsNAP [in BioFLL.LL.Syntax]
Syntax_LL.aForall [in BioFLL.LL.Syntax]
Syntax_LL.aQuest [in BioFLL.LL.Syntax]
Syntax_LL.aWith [in BioFLL.LL.Syntax]
Syntax_LL.aPar [in BioFLL.LL.Syntax]
Syntax_LL.aBot [in BioFLL.LL.Syntax]
Syntax_LL.aTop [in BioFLL.LL.Syntax]
Syntax_LL.eq_cons [in BioFLL.LL.Syntax]
Syntax_LL.eq_nil [in BioFLL.LL.Syntax]
Syntax_LL.eq_fx [in BioFLL.LL.Syntax]
Syntax_LL.eq_ex [in BioFLL.LL.Syntax]
Syntax_LL.eq_quest [in BioFLL.LL.Syntax]
Syntax_LL.eq_bang [in BioFLL.LL.Syntax]
Syntax_LL.eq_with [in BioFLL.LL.Syntax]
Syntax_LL.eq_plus [in BioFLL.LL.Syntax]
Syntax_LL.eq_par [in BioFLL.LL.Syntax]
Syntax_LL.eq_tensor [in BioFLL.LL.Syntax]
Syntax_LL.eq_one [in BioFLL.LL.Syntax]
Syntax_LL.eq_zero [in BioFLL.LL.Syntax]
Syntax_LL.eq_bot [in BioFLL.LL.Syntax]
Syntax_LL.eq_top [in BioFLL.LL.Syntax]
Syntax_LL.eq_perp [in BioFLL.LL.Syntax]
Syntax_LL.eq_atom [in BioFLL.LL.Syntax]
Syntax_LL.xva_ap [in BioFLL.LL.Syntax]
Syntax_LL.xvlt_cond [in BioFLL.LL.Syntax]
Syntax_LL.xvlt_nil [in BioFLL.LL.Syntax]
Syntax_LL.xvt_fc2 [in BioFLL.LL.Syntax]
Syntax_LL.xvt_fc1 [in BioFLL.LL.Syntax]
Syntax_LL.xvt_cte [in BioFLL.LL.Syntax]
Syntax_LL.xvt_var [in BioFLL.LL.Syntax]
Syntax_LL.cl_fx [in BioFLL.LL.Syntax]
Syntax_LL.cl_ex [in BioFLL.LL.Syntax]
Syntax_LL.cl_quest [in BioFLL.LL.Syntax]
Syntax_LL.cl_bang [in BioFLL.LL.Syntax]
Syntax_LL.cl_with [in BioFLL.LL.Syntax]
Syntax_LL.cl_plus [in BioFLL.LL.Syntax]
Syntax_LL.cl_par [in BioFLL.LL.Syntax]
Syntax_LL.cl_tensor [in BioFLL.LL.Syntax]
Syntax_LL.cl_top [in BioFLL.LL.Syntax]
Syntax_LL.cl_zero [in BioFLL.LL.Syntax]
Syntax_LL.cl_bot [in BioFLL.LL.Syntax]
Syntax_LL.cl_one [in BioFLL.LL.Syntax]
Syntax_LL.cl_perp [in BioFLL.LL.Syntax]
Syntax_LL.cl_atom [in BioFLL.LL.Syntax]
Syntax_LL.cl_ap [in BioFLL.LL.Syntax]
Syntax_LL.cl_fc2 [in BioFLL.LL.Syntax]
Syntax_LL.cl_fc1 [in BioFLL.LL.Syntax]
Syntax_LL.cl_cte [in BioFLL.LL.Syntax]
Syntax_LL.fx [in BioFLL.LL.Syntax]
Syntax_LL.ex [in BioFLL.LL.Syntax]
Syntax_LL.quest [in BioFLL.LL.Syntax]
Syntax_LL.bang [in BioFLL.LL.Syntax]
Syntax_LL.witH [in BioFLL.LL.Syntax]
Syntax_LL.plus [in BioFLL.LL.Syntax]
Syntax_LL.par [in BioFLL.LL.Syntax]
Syntax_LL.tensor [in BioFLL.LL.Syntax]
Syntax_LL.one [in BioFLL.LL.Syntax]
Syntax_LL.zero [in BioFLL.LL.Syntax]
Syntax_LL.bot [in BioFLL.LL.Syntax]
Syntax_LL.top [in BioFLL.LL.Syntax]
Syntax_LL.perp [in BioFLL.LL.Syntax]
Syntax_LL.atom [in BioFLL.LL.Syntax]
Syntax_LL.ap [in BioFLL.LL.Syntax]
Syntax_LL.fc2 [in BioFLL.LL.Syntax]
Syntax_LL.fc1 [in BioFLL.LL.Syntax]
Syntax_LL.cte [in BioFLL.LL.Syntax]
Syntax_LL.var [in BioFLL.LL.Syntax]

Inductive Index

P

plusOne [in BioFLL.Definitions]

S

SqSystems.Arrow [in BioFLL.LL.SequentCalculi]
SqSystems.TriSystem [in BioFLL.LL.SequentCalculi]
SqSystems.TriSystemh [in BioFLL.LL.SequentCalculi]
Syntax_LL.posFormula [in BioFLL.LL.Syntax]
Syntax_LL.posOrNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.NotAsynchronous [in BioFLL.LL.Syntax]
Syntax_LL.release [in BioFLL.LL.Syntax]
Syntax_LL.LexpPos' [in BioFLL.LL.Syntax]
Syntax_LL.IsPositiveAtom [in BioFLL.LL.Syntax]
Syntax_LL.IsNegativeAtom [in BioFLL.LL.Syntax]
Syntax_LL.Asynchronous [in BioFLL.LL.Syntax]
Syntax_LL.EqualUptoAtomsL [in BioFLL.LL.Syntax]
Syntax_LL.EqualUptoAtoms [in BioFLL.LL.Syntax]
Syntax_LL.xVariantA [in BioFLL.LL.Syntax]
Syntax_LL.xVariantLT [in BioFLL.LL.Syntax]
Syntax_LL.xVariantT [in BioFLL.LL.Syntax]
Syntax_LL.Closed [in BioFLL.LL.Syntax]
Syntax_LL.ClosedA [in BioFLL.LL.Syntax]
Syntax_LL.ClosedT [in BioFLL.LL.Syntax]
Syntax_LL.lexp [in BioFLL.LL.Syntax]
Syntax_LL.aprop [in BioFLL.LL.Syntax]
Syntax_LL.term [in BioFLL.LL.Syntax]

Instance Index

F

FormulasLL.lexpPos_morph [in BioFLL.LL.Syntax]

M

MultisetList.diff_morph [in BioFLL.LL.Multisets]
MultisetList.insert_morph [in BioFLL.LL.Multisets]
MultisetList.member_morph [in BioFLL.LL.Multisets]
MultisetList.meq_Equivalence [in BioFLL.LL.Multisets]
MultisetList.mult_morph [in BioFLL.LL.Multisets]
MultisetList.remove_morph [in BioFLL.LL.Multisets]
MultisetList.rem_morph [in BioFLL.LL.Multisets]
MultisetList.union_morph' [in BioFLL.LL.Multisets]
MultisetList.union_morph [in BioFLL.LL.Multisets]

S

SqBasic.trih_morph' [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.trih_morphh [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.tri_morph' [in BioFLL.LL.SequentCalculiBasicTheory]
SqBasic.tri_morph [in BioFLL.LL.SequentCalculiBasicTheory]

Section Index

M

MultisetList.Decidability [in BioFLL.LL.Multisets]
MultisetList.meq_equivalence [in BioFLL.LL.Multisets]
MultisetList.Multiset [in BioFLL.LL.Multisets]

S

StrongIndPrinciple [in BioFLL.LL.StrongInduction]
Syntax_LL.Polarities [in BioFLL.LL.Syntax]
Syntax_LL.EqUpTo [in BioFLL.LL.Syntax]
Syntax_LL.Measures [in BioFLL.LL.Syntax]
Syntax_LL.EqualityFormulas [in BioFLL.LL.Syntax]
Syntax_LL.Substitution [in BioFLL.LL.Syntax]
Syntax_LL.Dualities [in BioFLL.LL.Syntax]
Syntax_LL.Sec_lExp [in BioFLL.LL.Syntax]

Definition Index

B

bleccm0 [in BioFLL.Definitions]
bleccm1 [in BioFLL.Definitions]
bleccm2 [in BioFLL.Definitions]
blecc0 [in BioFLL.Definitions]
blecc1 [in BioFLL.Definitions]
blecc2 [in BioFLL.Definitions]
blecm0 [in BioFLL.Definitions]
blecm1 [in BioFLL.Definitions]
blecm2 [in BioFLL.Definitions]
blec0 [in BioFLL.Definitions]
blec1 [in BioFLL.Definitions]
blec2 [in BioFLL.Definitions]
blec3 [in BioFLL.Definitions]
ble0 [in BioFLL.Definitions]
ble0r [in BioFLL.Definitions]
ble1 [in BioFLL.Definitions]
ble2 [in BioFLL.Definitions]
blood [in BioFLL.Definitions]
bone [in BioFLL.Definitions]
bo0 [in BioFLL.Definitions]
bo1 [in BioFLL.Definitions]
bo2 [in BioFLL.Definitions]
breast [in BioFLL.Definitions]
bre0 [in BioFLL.Definitions]
bre0r [in BioFLL.Definitions]
bre1 [in BioFLL.Definitions]
bre2 [in BioFLL.Definitions]
brt0 [in BioFLL.Definitions]
brt0r [in BioFLL.Definitions]
brt1 [in BioFLL.Definitions]
brt2 [in BioFLL.Definitions]
br0 [in BioFLL.Definitions]
br1 [in BioFLL.Definitions]
br2 [in BioFLL.Definitions]

C

CD44 [in BioFLL.Definitions]
CD47 [in BioFLL.Definitions]

D

d00 [in BioFLL.Definitions]
d01 [in BioFLL.Definitions]
d02 [in BioFLL.Definitions]
d10 [in BioFLL.Definitions]
d10r [in BioFLL.Definitions]
d11 [in BioFLL.Definitions]
d12 [in BioFLL.Definitions]
d20 [in BioFLL.Definitions]
d20r [in BioFLL.Definitions]
d21 [in BioFLL.Definitions]
d22 [in BioFLL.Definitions]
d30 [in BioFLL.Definitions]
d30r [in BioFLL.Definitions]
d31 [in BioFLL.Definitions]
d32 [in BioFLL.Definitions]
d40 [in BioFLL.Definitions]
d41 [in BioFLL.Definitions]
d42 [in BioFLL.Definitions]
d43 [in BioFLL.Definitions]
d50 [in BioFLL.Definitions]
d51 [in BioFLL.Definitions]
d52 [in BioFLL.Definitions]
d60 [in BioFLL.Definitions]
d61 [in BioFLL.Definitions]
d62 [in BioFLL.Definitions]
d70 [in BioFLL.Definitions]
d71 [in BioFLL.Definitions]
d72 [in BioFLL.Definitions]
d80 [in BioFLL.Definitions]
d81 [in BioFLL.Definitions]
d82 [in BioFLL.Definitions]

E

EncodeRule [in BioFLL.Definitions]
EncodeRuleAP [in BioFLL.Definitions]
EP [in BioFLL.Definitions]
EPCAM [in BioFLL.Definitions]
EPCD [in BioFLL.Definitions]
EPCDCD [in BioFLL.Definitions]
EPCDCDME [in BioFLL.Definitions]
EPCDCDMEse [in BioFLL.Definitions]
EPCDME [in BioFLL.Definitions]

F

FormulasLL.lexp_eq.eqA_dec [in BioFLL.LL.Syntax]
FormulasLL.lexp_eq.A [in BioFLL.LL.Syntax]

G

GenRs [in BioFLL.Definitions]
GoalP5 [in BioFLL.MetaLevelProperties]

L

ListPosAtom [in BioFLL.Utils]

M

MET [in BioFLL.Definitions]
MultisetList.diff [in BioFLL.LL.Multisets]
MultisetList.empty [in BioFLL.LL.Multisets]
MultisetList.member [in BioFLL.LL.Multisets]
MultisetList.meq [in BioFLL.LL.Multisets]
MultisetList.mult [in BioFLL.LL.Multisets]
MultisetList.Multiset [in BioFLL.LL.Multisets]
MultisetList.rem [in BioFLL.LL.Multisets]
MultisetList.removeAll [in BioFLL.LL.Multisets]
MultisetList.removeElem [in BioFLL.LL.Multisets]
MultisetList.singleton [in BioFLL.LL.Multisets]
MultisetList.union [in BioFLL.LL.Multisets]

N

NatSet.A [in BioFLL.LL.Eqset]
NatSet.eqA_dec [in BioFLL.LL.Eqset]
NatSet.isPositive [in BioFLL.LL.Eqset]
NONE [in BioFLL.Definitions]

S

seeded [in BioFLL.Definitions]
SqSystems.Arrow2LL [in BioFLL.LL.SequentCalculi]
Syntax_LL.PosFormula [in BioFLL.LL.Syntax]
Syntax_LL.PosOrNegAtom [in BioFLL.LL.Syntax]
Syntax_LL.Release [in BioFLL.LL.Syntax]
Syntax_LL.BlexpPos [in BioFLL.LL.Syntax]
Syntax_LL.LexpPos [in BioFLL.LL.Syntax]
Syntax_LL.L_weight [in BioFLL.LL.Syntax]
Syntax_LL.Exp_weight [in BioFLL.LL.Syntax]
Syntax_LL.exp_weight [in BioFLL.LL.Syntax]
Syntax_LL.AsynchronousF [in BioFLL.LL.Syntax]
Syntax_LL.asynchronousF [in BioFLL.LL.Syntax]
Syntax_LL.eq_wt [in BioFLL.LL.Syntax]
Syntax_LL.Lexp_weight [in BioFLL.LL.Syntax]
Syntax_LL.lexp_weight [in BioFLL.LL.Syntax]
Syntax_LL.SubstL [in BioFLL.LL.Syntax]
Syntax_LL.Subst [in BioFLL.LL.Syntax]
Syntax_LL.flatten [in BioFLL.LL.Syntax]
Syntax_LL.flattenT [in BioFLL.LL.Syntax]
Syntax_LL.Dual_LExp [in BioFLL.LL.Syntax]
Syntax_LL.Imp [in BioFLL.LL.Syntax]
Syntax_LL.imp [in BioFLL.LL.Syntax]
Syntax_LL.dual_LExp [in BioFLL.LL.Syntax]
Syntax_LL.Fx [in BioFLL.LL.Syntax]
Syntax_LL.Ex [in BioFLL.LL.Syntax]
Syntax_LL.Quest [in BioFLL.LL.Syntax]
Syntax_LL.Bang [in BioFLL.LL.Syntax]
Syntax_LL.With [in BioFLL.LL.Syntax]
Syntax_LL.Plus [in BioFLL.LL.Syntax]
Syntax_LL.Par [in BioFLL.LL.Syntax]
Syntax_LL.Tensor [in BioFLL.LL.Syntax]
Syntax_LL.Zero [in BioFLL.LL.Syntax]
Syntax_LL.One [in BioFLL.LL.Syntax]
Syntax_LL.Bot [in BioFLL.LL.Syntax]
Syntax_LL.Top [in BioFLL.LL.Syntax]
Syntax_LL.Perp [in BioFLL.LL.Syntax]
Syntax_LL.Atom [in BioFLL.LL.Syntax]
Syntax_LL.AP [in BioFLL.LL.Syntax]
Syntax_LL.FC2 [in BioFLL.LL.Syntax]
Syntax_LL.FC1 [in BioFLL.LL.Syntax]
Syntax_LL.Cte [in BioFLL.LL.Syntax]
Syntax_LL.SubsL [in BioFLL.LL.Syntax]
Syntax_LL.Subs [in BioFLL.LL.Syntax]
Syntax_LL.Lexp [in BioFLL.LL.Syntax]
Syntax_LL.AProp [in BioFLL.LL.Syntax]
Syntax_LL.LTerm [in BioFLL.LL.Syntax]
Syntax_LL.Term [in BioFLL.LL.Syntax]

T

TG [in BioFLL.Definitions]
TGFbeta [in BioFLL.Definitions]
Theory [in BioFLL.Definitions]

Global Index

H

J

K

O

Q

V

W

X

Y

Z

_

(797 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(33 entries)

Module Index

A

B

C

D

G

H

I

J

K

L

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(16 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(8 entries)

Library Index

A

B

C

F

G

H

J

K

L

N

O

P

Q

T

V

W

X

Y

Z

_

other

(11 entries)

Lemma Index

B

C

D

H

J

K

L

N

O

Q

R

U

V

W

X

Y

Z

_

other

(373 entries)

Axiom Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(12 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(149 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

other

(23 entries)

Instance Index

A

B

C

D

E

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(11 entries)

Definition Index

A

H

I

J

K

O

P

Q

R

U

V

W

X

Y

Z

_

other

(147 entries)

This page has been generated by coqdoc