kdrag.theories.algebra

Functions

check_semigroup(S)

Classes

AddSemigroup(*args, **kwargs)
CommAddSemigroup(*args, **kwargs)
CommSemigroup(*args, **kwargs)
Group(*args, **kwargs)	A Group is a Monoid with an inverse element.
Monoid(*args, **kwargs)	A Monoid is a Semigroup with an identity element.
SemiGroup(*args, **kwargs)	A Semigroup is a set with an associative binary operation.

class kdrag.theories.algebra.AddSemigroup(*args, **kwargs)

Bases: Protocol

add: FuncDeclRef

add_assoc: Proof

class kdrag.theories.algebra.CommAddSemigroup(*args, **kwargs)

Bases: AddSemigroup, Protocol

add: FuncDeclRef

add_assoc: Proof

add_comm: Proof

class kdrag.theories.algebra.CommSemigroup(*args, **kwargs)

Bases: SemiGroup, Protocol

mul: FuncDeclRef

mul_assoc: Proof

mul_comm: Proof

class kdrag.theories.algebra.Group(*args, **kwargs)

Bases: Monoid, Protocol

A Group is a Monoid with an inverse element. mul_left_inv : forall x, inv x * x = one mul_right_inv : forall x, x * inv x = one

inv: FuncDeclRef

mul: FuncDeclRef

mul_assoc: Proof

mul_left_inv: Proof

mul_one: Proof

mul_right_inv: Proof

one: ExprRef

one_mul: Proof

class kdrag.theories.algebra.Monoid(*args, **kwargs)

Bases: SemiGroup, Protocol

A Monoid is a Semigroup with an identity element. one_mul : forall x, one * x = x mul_one : forall x, x * one = x

mul: FuncDeclRef

mul_assoc: Proof

mul_one: Proof

one: ExprRef

one_mul: Proof

class kdrag.theories.algebra.SemiGroup(*args, **kwargs)

Bases: Protocol

A Semigroup is a set with an associative binary operation. mul_assoc : forall x y z, mul (mul x y)

mul: FuncDeclRef

mul_assoc: Proof

kdrag.theories.algebra.check_semigroup(S: SemiGroup)

Parameters:

S (SemiGroup)

Modules

category
filter
group
kleene
lattice
ordering
sqmatrix
topology
vector