Commit 7e7b10c3 authored by root's avatar root

update

parent 91dd65ff
theory cic:/functional_algebra?commutative_ring
HasMeta cic:/functional_algebra?commutative_ring http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?ring
Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?abelian_group
Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?group
Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?monoid
......@@ -7,28 +8,18 @@ Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?functi
Includes cic:/functional_algebra?commutative_ring cic:/functional_algebra?base
Includes cic:/functional_algebra?commutative_ring cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/functional_algebra?commutative_ring cic:/Coq/Logic?Description
Includes cic:/functional_algebra?commutative_ring http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/functional_algebra?commutative_ring cic:/functional_algebra?commutative_ring?Commutative_Ring
theory cic:/functional_algebra?commutative_ring/Commutative_Ring
HasMeta cic:/functional_algebra?commutative_ring/Commutative_Ring http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?function
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Specif
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Notations/IfNotations
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Notations
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?group/Group
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?ring/Ring
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?abelian_group/Abelian_Group
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Logic?Description
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?monoid/Monoid
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Logic/EqNotations
Includes cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/Coq/Init?Logic
Declares cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?commutative_ring/Commutative_Ring?Commutative_Ring_DEF
deriveddeclaration cic:/functional_algebra?commutative_ring/Commutative_Ring?Commutative_Ring_DEF
Declares cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?commutative_ring/Commutative_Ring?Commutative_Ring
constant cic:/functional_algebra?commutative_ring/Commutative_Ring?Commutative_Ring
Declares cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?commutative_ring/Commutative_Ring?commutative_ring
constant cic:/functional_algebra?commutative_ring/Commutative_Ring?commutative_ring
IsAliasFor cic:/functional_algebra?commutative_ring/Commutative_Ring?Commutative_Ring_C_1 cic:/functional_algebra?commutative_ring/Commutative_Ring?commutative_ring
Declares cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?commutative_ring/Commutative_Ring?E
constant cic:/functional_algebra?commutative_ring/Commutative_Ring?E
Declares cic:/functional_algebra?commutative_ring/Commutative_Ring cic:/functional_algebra?commutative_ring/Commutative_Ring?E_0
......
theory cic:/functional_algebra?field
HasMeta cic:/functional_algebra?field http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?field cic:/functional_algebra?commutative_ring
Includes cic:/functional_algebra?field cic:/functional_algebra?ring
Includes cic:/functional_algebra?field cic:/functional_algebra?abelian_group
Includes cic:/functional_algebra?field cic:/functional_algebra?group
Includes cic:/functional_algebra?field cic:/functional_algebra?monoid_group
Includes cic:/functional_algebra?field cic:/functional_algebra?monoid
Includes cic:/functional_algebra?field cic:/functional_algebra?function
Includes cic:/functional_algebra?field cic:/functional_algebra?base
Includes cic:/functional_algebra?field cic:/Coq/Logic?Description
Includes cic:/functional_algebra?field cic:/Coq/Logic?Eqdep
Includes cic:/functional_algebra?field http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/functional_algebra?field cic:/functional_algebra?field?Field
theory cic:/functional_algebra?field/Field
HasMeta cic:/functional_algebra?field/Field http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?field/Field cic:/Coq/Logic?EqdepFacts
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?commutative_ring/Commutative_Ring
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?function
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Specif
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Notations/IfNotations
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Notations
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?group/Group
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?abelian_group/Abelian_Group
Includes cic:/functional_algebra?field/Field cic:/Coq/Bool?Bool
Includes cic:/functional_algebra?field/Field cic:/Coq/Classes?Init
Includes cic:/functional_algebra?field/Field cic:/Coq/Classes?Morphisms/ProperNotations
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?PeanoNat/Nat/Private_Parity
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?PeanoNat/Nat
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?EqNat
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Factorial
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Compare_dec
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Peano_dec
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Between
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Mult
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Minus
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Gt
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Plus
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Lt
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Le
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?PeanoNat
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Arith_base
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Arith
Includes cic:/functional_algebra?field/Field cic:/Coq/Classes?Morphisms
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Decimal/Little
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Decimal
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Nat
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Peano
Includes cic:/functional_algebra?field/Field cic:/Coq/Arith?Wf_nat
Includes cic:/functional_algebra?field/Field cic:/Coq/Classes?RelationClasses
Includes cic:/functional_algebra?field/Field cic:/Coq/Logic?ChoiceFacts
Includes cic:/functional_algebra?field/Field cic:/Coq/Logic?Description
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Specif
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?function
Includes cic:/functional_algebra?field/Field cic:/Coq/Logic?Description
Includes cic:/functional_algebra?field/Field cic:/Coq/Logic?FunctionalExtensionality
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?ring/Ring
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?abelian_group/Abelian_Group
Includes cic:/functional_algebra?field/Field cic:/functional_algebra?monoid/Monoid
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Notations/IfNotations
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Notations
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Logic/EqNotations
Includes cic:/functional_algebra?field/Field cic:/Coq/Init?Logic
Declares cic:/functional_algebra?field/Field cic:/functional_algebra?field/Field?Field_DEF
......
......@@ -3,6 +3,7 @@ dataconstructor cic:/functional_algebra?function?is_onto
dataconstructor cic:/functional_algebra?function?is_bijective
theory cic:/functional_algebra?function
HasMeta cic:/functional_algebra?function http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?function cic:/Coq/Init?Logic
Declares cic:/functional_algebra?function cic:/functional_algebra?function?is_injective
constant cic:/functional_algebra?function?is_injective
Declares cic:/functional_algebra?function cic:/functional_algebra?function?is_onto
......
theory cic:/functional_algebra?group
HasMeta cic:/functional_algebra?group http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?group cic:/functional_algebra?monoid
Includes cic:/functional_algebra?group cic:/Coq/Logic?ProofIrrelevance
Includes cic:/functional_algebra?group cic:/Coq/Logic?Description
Includes cic:/functional_algebra?group cic:/functional_algebra?base
Includes cic:/functional_algebra?group cic:/functional_algebra?function
Includes cic:/functional_algebra?group cic:/functional_algebra?monoid
Declares cic:/functional_algebra?group cic:/functional_algebra?group?Group
theory cic:/functional_algebra?group/Group
HasMeta cic:/functional_algebra?group/Group http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?group/Group cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?group/Group cic:/Coq/Init?Specif
Includes cic:/functional_algebra?group/Group cic:/Coq/Logic?Description
Includes cic:/functional_algebra?group/Group cic:/Coq/Init?Logic
Includes cic:/functional_algebra?group/Group cic:/functional_algebra?monoid/Monoid
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?Group_DEF
deriveddeclaration cic:/functional_algebra?group/Group?Group_DEF
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?Group
constant cic:/functional_algebra?group/Group?Group
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?group
constant cic:/functional_algebra?group/Group?group
IsAliasFor cic:/functional_algebra?group/Group?Group_C_1 cic:/functional_algebra?group/Group?group
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?E
constant cic:/functional_algebra?group/Group?E
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?E_0
......@@ -38,64 +28,4 @@ Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group
constant cic:/functional_algebra?group/Group?op_inv_r_ex
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?Theorems
deriveddeclaration cic:/functional_algebra?group/Group?Theorems
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_monoid
constant cic:/functional_algebra?group/Group?op_monoid
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_id_l
constant cic:/functional_algebra?group/Group?op_is_id_l
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_id_r
constant cic:/functional_algebra?group/Group?op_is_id_r
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_id
constant cic:/functional_algebra?group/Group?op_is_id
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_id
constant cic:/functional_algebra?group/Group?op_id
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_inv_l
constant cic:/functional_algebra?group/Group?op_is_inv_l
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_inv_r
constant cic:/functional_algebra?group/Group?op_is_inv_r
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_id_l_uniq
constant cic:/functional_algebra?group/Group?op_id_l_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_id_r_uniq
constant cic:/functional_algebra?group/Group?op_id_r_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_id_uniq
constant cic:/functional_algebra?group/Group?op_id_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_intro_l
constant cic:/functional_algebra?group/Group?op_intro_l
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_intro_r
constant cic:/functional_algebra?group/Group?op_intro_r
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_is_inv
constant cic:/functional_algebra?group/Group?op_is_inv
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_l_r_eq
constant cic:/functional_algebra?group/Group?op_inv_l_r_eq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_sym
constant cic:/functional_algebra?group/Group?op_inv_sym
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_ex
constant cic:/functional_algebra?group/Group?op_inv_ex
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_cancel_l
constant cic:/functional_algebra?group/Group?op_cancel_l
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_cancel_r
constant cic:/functional_algebra?group/Group?op_cancel_r
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_l_uniq
constant cic:/functional_algebra?group/Group?op_inv_l_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_r_uniq
constant cic:/functional_algebra?group/Group?op_inv_r_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_uniq
constant cic:/functional_algebra?group/Group?op_inv_uniq
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_inv_uniq_ex
constant cic:/functional_algebra?group/Group?op_inv_uniq_ex
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_strong
constant cic:/functional_algebra?group/Group?op_neg_strong
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg
constant cic:/functional_algebra?group/Group?op_neg
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_def
constant cic:/functional_algebra?group/Group?op_neg_def
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_inj
constant cic:/functional_algebra?group/Group?op_neg_inj
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_cancel_neg
constant cic:/functional_algebra?group/Group?op_cancel_neg
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_onto
constant cic:/functional_algebra?group/Group?op_neg_onto
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_bijective
constant cic:/functional_algebra?group/Group?op_neg_bijective
Declares cic:/functional_algebra?group/Group cic:/functional_algebra?group/Group?op_neg_rev
constant cic:/functional_algebra?group/Group?op_neg_rev
Includes cic:/functional_algebra?group cic:/functional_algebra?group/Group
theory cic:/functional_algebra?group_expr
HasMeta cic:/functional_algebra?group_expr http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?group_expr cic:/functional_algebra?group
Includes cic:/functional_algebra?group_expr cic:/functional_algebra?monoid_expr
Includes cic:/functional_algebra?group_expr cic:/functional_algebra?monoid
Includes cic:/functional_algebra?group_expr cic:/functional_algebra?base
Includes cic:/functional_algebra?group_expr http://coq.inria.fr/foundation?CoqSyntax
Declares cic:/functional_algebra?group_expr cic:/functional_algebra?group_expr?GroupExpr
theory cic:/functional_algebra?group_expr/GroupExpr
HasMeta cic:/functional_algebra?group_expr/GroupExpr http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/Coq/Init?Specif
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/Coq/Init?Logic
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/functional_algebra?monoid_expr/MonoidExpr
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/functional_algebra?monoid/Monoid
Includes cic:/functional_algebra?group_expr/GroupExpr cic:/functional_algebra?group/Group
Declares cic:/functional_algebra?group_expr/GroupExpr cic:/functional_algebra?group_expr/GroupExpr?g
......
theory cic:/functional_algebra?monoid_expr
HasMeta cic:/functional_algebra?monoid_expr http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Init?Specif
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Init?Logic
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid/Monoid
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Bool?Bool
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Logic?ProofIrrelevance
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?function
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?base
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Logic?Description
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?base
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?function
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Logic?ProofIrrelevance
Includes cic:/functional_algebra?monoid_expr cic:/Coq/Bool?Bool
Includes cic:/functional_algebra?monoid_expr http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid
Declares cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid_expr?MonoidExpr
theory cic:/functional_algebra?monoid_expr/MonoidExpr
HasMeta cic:/functional_algebra?monoid_expr/MonoidExpr http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/Coq/Bool?Bool
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/Coq/Init?Specif
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid/Monoid
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/Coq/Init?Logic/EqNotations
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/Coq/Init?Logic
Includes cic:/functional_algebra?monoid_expr/MonoidExpr cic:/Coq/Init?Datatypes
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Definitions
deriveddeclaration cic:/functional_algebra?monoid_expr/MonoidExpr?Definitions
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_node
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_node
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_leaf
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_leaf
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_rassoc
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_is_rassoc
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_rassoc_thm
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_rassoc_thm
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_map_DEF
deriveddeclaration cic:/functional_algebra?monoid_expr/MonoidExpr?Term_map_DEF
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_map
constant cic:/functional_algebra?monoid_expr/MonoidExpr?Term_map
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?term_map
constant cic:/functional_algebra?monoid_expr/MonoidExpr?term_map
IsAliasFor cic:/functional_algebra?monoid_expr/MonoidExpr?Term_map_C_1 cic:/functional_algebra?monoid_expr/MonoidExpr?term_map
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?term_map_m
constant cic:/functional_algebra?monoid_expr/MonoidExpr?term_map_m
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?term_map_term
......@@ -49,36 +26,8 @@ Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?
constant cic:/functional_algebra?monoid_expr/MonoidExpr?term_map_is_zero_thm
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Functions
deriveddeclaration cic:/functional_algebra?monoid_expr/MonoidExpr?Functions
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_nonzero
constant cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_nonzero
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_eval
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_eval
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_eq
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_eq
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_shift
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_shift
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_rassoc
constant cic:/functional_algebra?monoid_expr/MonoidExpr?BTree_rassoc
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?list_eval
constant cic:/functional_algebra?monoid_expr/MonoidExpr?list_eval
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?list_eq
constant cic:/functional_algebra?monoid_expr/MonoidExpr?list_eq
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?RABTree_list
constant cic:/functional_algebra?monoid_expr/MonoidExpr?RABTree_list
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?list_filter_0
constant cic:/functional_algebra?monoid_expr/MonoidExpr?list_filter_0
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?reduce
constant cic:/functional_algebra?monoid_expr/MonoidExpr?reduce
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Theorems
deriveddeclaration cic:/functional_algebra?monoid_expr/MonoidExpr?Theorems
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_eval
constant cic:/functional_algebra?monoid_expr/MonoidExpr?Term_eval
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_zero
constant cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_zero
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_zero_thm
constant cic:/functional_algebra?monoid_expr/MonoidExpr?Term_is_zero_thm
Declares cic:/functional_algebra?monoid_expr/MonoidExpr cic:/functional_algebra?monoid_expr/MonoidExpr?MTerm_map
constant cic:/functional_algebra?monoid_expr/MonoidExpr?MTerm_map
Includes cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid_expr/MonoidExpr
Declares cic:/functional_algebra?monoid_expr cic:/functional_algebra?monoid_expr?Unittests
deriveddeclaration cic:/functional_algebra?monoid_expr?Unittests
theory cic:/functional_algebra?monoid_group
HasMeta cic:/functional_algebra?monoid_group http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?monoid_group cic:/Coq/Logic?Eqdep
Includes cic:/functional_algebra?monoid_group cic:/functional_algebra?group
Includes cic:/functional_algebra?monoid_group cic:/functional_algebra?monoid
Includes cic:/functional_algebra?monoid_group cic:/functional_algebra?base
Includes cic:/functional_algebra?monoid_group cic:/functional_algebra?monoid
Includes cic:/functional_algebra?monoid_group cic:/functional_algebra?group
Includes cic:/functional_algebra?monoid_group cic:/Coq/Logic?Eqdep
Declares cic:/functional_algebra?monoid_group cic:/functional_algebra?monoid_group?Monoid_Group
theory cic:/functional_algebra?monoid_group/Monoid_Group
HasMeta cic:/functional_algebra?monoid_group/Monoid_Group http://coq.inria.fr/foundation?CoqSyntax
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Datatypes
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Logic?Description
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?group/Group
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Logic/EqNotations
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Notations/IfNotations
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Notations
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Logic?EqdepFacts/EqdepTheory
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Logic?EqdepFacts
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Logic
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/Coq/Init?Specif
Includes cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid/Monoid
Declares cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid_group/Monoid_Group?Monoid_Group_DEF
deriveddeclaration cic:/functional_algebra?monoid_group/Monoid_Group?Monoid_Group_DEF
Declares cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid_group/Monoid_Group?Monoid_Group
constant cic:/functional_algebra?monoid_group/Monoid_Group?Monoid_Group
Declares cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid_group/Monoid_Group?monoid_group
constant cic:/functional_algebra?monoid_group/Monoid_Group?monoid_group
IsAliasFor cic:/functional_algebra?monoid_group/Monoid_Group?Monoid_Group_C_1 cic:/functional_algebra?monoid_group/Monoid_Group?monoid_group
Declares cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid_group/Monoid_Group?E
constant cic:/functional_algebra?monoid_group/Monoid_Group?E
Declares cic:/functional_algebra?monoid_group/Monoid_Group cic:/functional_algebra?monoid_group/Monoid_Group?E_0
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment