name: "struct_analysis";
version: "0.1.0";
description: "add your description here";
functions {
  associative : associative';
  associative_from : sym(p, all(p'(p'(a, b), c) == p'(a, p'(b, c))))(p) -> associative'(p);
  associative_prop_and : true -> associative'(prop_and');
  associative_prop_eq_excm : Excm' -> associative'(prop_eq');
  associative_prop_or : true -> associative'(prop_or');
  associative_to : associative'(p) -> sym(p, all(p'(p'(a, b), c) == p'(a, p'(b, c))))(p);
  commutative : commutative';
  commutative_from : sym(p, all(p'(a, b) == p'(b, a)))(p) -> commutative'(p);
  commutative_prop_and : true -> commutative'(prop_and');
  commutative_prop_eq : true -> commutative'(prop_eq');
  commutative_prop_or : true -> commutative'(prop_or');
  commutative_q : true -> commutative'(q');
  commutative_to : commutative'(p) -> sym(p, all(p'(a, b) == p'(b, a)))(p);
  reflexive : reflexive';
  reflexive_from : sym(p, all(p'(a, a)))(p) -> reflexive'(p);
  reflexive_prop_eq : true -> reflexive'(prop_eq');
  reflexive_prop_imply : true -> reflexive'(prop_imply');
  reflexive_to : reflexive'(p) -> sym(p, all(p'(a, a)))(p);
  transitive : transitive';
  transitive_from : sym(p, all((p'(a, b) & p'(b, c)) => p'(a, c)))(p) -> transitive'(p);
  transitive_prop_and : true -> transitive'(prop_and');
  transitive_prop_imply : true -> transitive'(prop_imply');
  transitive_to : transitive'(p) -> sym(p, all((p'(a, b) & p'(b, c)) => p'(a, c)))(p);
  transitivie_prop_eq : true -> transitive'(prop_eq');
  transitivity_q : true -> transitive'(q');
}
dependencies {
}