# Path: calculus/variable.py
# class GeneralizedVariable:
# class Variable(GeneralizedVariable):
# class StringVariable(Variable):
# class ApplySymbolVariable(GeneralizedVariable):
# class ProductVariable(GeneralizedVariable):
#   def simplify(self):
#   def render(self):
#   def applied_variables(self):
#   def relatedVariable(self):
#   def __init__(self):
#   def _generate_id(self):
#   def updateVariables(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def __hash__(self):
#   def applied_variables(self):
#   def __repr__(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def __init__(self, name, infix = None):
#   def relatedVariable(self):
#   def render(self):
#   def name(self):
#   def __repr__(self):
#   def updateVariables(self):
# def renderInfix(productVariable, infixSymbols, infixVariable):
#   def __init__(self, variable, symbol):
#   def __eq__(self, other):
#   def applied_variables(self):
#   def __ne__(self, other):
#   def __repr__(self):
#   def updateVariables(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def render(self):
# def colors_for_symbol(symbol):
#   def __init__(self, symbol_variable_pairs):
#   def applied_variables(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def __repr__(self):
#   def updateVariables(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def render(self):
# def renderSymbolVariablePair(s, v, c0, c1):
# def borderStack(dimension, color, a, b, borderWidth):
# def renderSymbol(s):
# def renderStringSymbol(s):
# def renderWithBackground(s, border_width, color):
# 
# Path: calculus/enriched/constructors.py
# def Holds(held, holding):
# def And(values):
# def Or(values):
# def Not(value):
# def Apply(v, x):
# def Identical(left, right):
# def OrdinaryVariableBinding(variable):
# def BoundedVariableBinding(variable, relation):
# def WelldefinedVariableBinding(variable, relation):
# def Exists(bindings, value):
# def Forall(bindings, value):
# def Always(value):
# def Maybe(value):
# def Implies(predicates, consequent):
# def Equal(a, b):
# def S(a):
# def Iff(left, right):
# def Hidden(value, name):
# def assume(x, B):
# 
# Path: lib/library.py
# class Library:
# class Proof:
#   def __init__(self, claims, variables, sub_libraries, name = None):
#   def __hash__(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def all_libraries_recursively(self):
#   def formula(self):
#   def beginProof(self):
#   def __init__(self, library, arrow = None):
#   def translate(self):
#   def forwardFollow(self, f):
# 
# Path: lib/common_vars.py
# A = lambda: StringVariable('A')
# B = lambda: StringVariable('B')
# C = lambda: StringVariable('C')
# R = lambda: StringVariable('R')
# S = variable.StringVariable('S')
# 
# Path: lib/common_symbols.py

# 
# Path: lib/common_formulas.py
# def IsEquivalence(e):
# def Maps(a, b, f):
# def IsFunction(f):
# def InductionBase(var, claim):
# def InductionStep(var, claim):
# def InductionHypotheses(var, claim):
# def InductionConclusion(var, claim):
# def Induction(var, claim):
# def _forwardImportInduction(x, var, claim):
# def forwardImportInductionAndContradict(x, var, claim):
# def forwardInductionOnIExists(x, i):


from calculus import variable
from calculus.enriched import constructors
from lib import library, common_vars
from lib.common_symbols import leftSymbol, rightSymbol, relationSymbol, domainSymbol
from lib.common_formulas import InDomain, Equal, IsEquivalence


x = common_vars.x()
def reflexive(e):
  return constructors.Forall([constructors.BoundedVariableBinding(x, e)],
      Equal(x, x, e))

x = common_vars.x()
y = common_vars.y()
def symmetric(e):
  return constructors.Forall([ constructors.BoundedVariableBinding(x, e)
                             , constructors.BoundedVariableBinding(y, e)],
      constructors.Implies(
        predicates = [Equal(x, y, e)],
        consequent = Equal(y, x, e)))

x = common_vars.x()
y = common_vars.y()
z = common_vars.z()
def transitive(e):
  return constructors.Forall([ constructors.BoundedVariableBinding(x, e)
                             , constructors.BoundedVariableBinding(y, e)
                             , constructors.BoundedVariableBinding(z, e)],
      constructors.Implies(
        predicates = [ Equal(x, y, e)
                     , Equal(y, z, e) ],
        consequent = Equal(x, z, e)))

A = common_vars.A()
claim = constructors.Forall([constructors.OrdinaryVariableBinding(A)],

# Path: calculus/variable.py
# class GeneralizedVariable:
# class Variable(GeneralizedVariable):
# class StringVariable(Variable):
# class ApplySymbolVariable(GeneralizedVariable):
# class ProductVariable(GeneralizedVariable):
#   def simplify(self):
#   def render(self):
#   def applied_variables(self):
#   def relatedVariable(self):
#   def __init__(self):
#   def _generate_id(self):
#   def updateVariables(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def __hash__(self):
#   def applied_variables(self):
#   def __repr__(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def __init__(self, name, infix = None):
#   def relatedVariable(self):
#   def render(self):
#   def name(self):
#   def __repr__(self):
#   def updateVariables(self):
# def renderInfix(productVariable, infixSymbols, infixVariable):
#   def __init__(self, variable, symbol):
#   def __eq__(self, other):
#   def applied_variables(self):
#   def __ne__(self, other):
#   def __repr__(self):
#   def updateVariables(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def render(self):
# def colors_for_symbol(symbol):
#   def __init__(self, symbol_variable_pairs):
#   def applied_variables(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def __repr__(self):
#   def updateVariables(self):
#   def substituteVariable(self, a, b):
#   def freeVariables(self):
#   def render(self):
# def renderSymbolVariablePair(s, v, c0, c1):
# def borderStack(dimension, color, a, b, borderWidth):
# def renderSymbol(s):
# def renderStringSymbol(s):
# def renderWithBackground(s, border_width, color):
# 
# Path: calculus/enriched/constructors.py
# def Holds(held, holding):
# def And(values):
# def Or(values):
# def Not(value):
# def Apply(v, x):
# def Identical(left, right):
# def OrdinaryVariableBinding(variable):
# def BoundedVariableBinding(variable, relation):
# def WelldefinedVariableBinding(variable, relation):
# def Exists(bindings, value):
# def Forall(bindings, value):
# def Always(value):
# def Maybe(value):
# def Implies(predicates, consequent):
# def Equal(a, b):
# def S(a):
# def Iff(left, right):
# def Hidden(value, name):
# def assume(x, B):
# 
# Path: lib/library.py
# class Library:
# class Proof:
#   def __init__(self, claims, variables, sub_libraries, name = None):
#   def __hash__(self):
#   def __eq__(self, other):
#   def __ne__(self, other):
#   def all_libraries_recursively(self):
#   def formula(self):
#   def beginProof(self):
#   def __init__(self, library, arrow = None):
#   def translate(self):
#   def forwardFollow(self, f):
# 
# Path: lib/common_vars.py
# A = lambda: StringVariable('A')
# B = lambda: StringVariable('B')
# C = lambda: StringVariable('C')
# R = lambda: StringVariable('R')
# S = variable.StringVariable('S')
# 
# Path: lib/common_symbols.py

# 
# Path: lib/common_formulas.py
# def IsEquivalence(e):
# def Maps(a, b, f):
# def IsFunction(f):
# def InductionBase(var, claim):
# def InductionStep(var, claim):
# def InductionHypotheses(var, claim):
# def InductionConclusion(var, claim):
# def Induction(var, claim):
# def _forwardImportInduction(x, var, claim):
# def forwardImportInductionAndContradict(x, var, claim):
# def forwardInductionOnIExists(x, i):


# Path: lib/equivalence.py
from calculus import variable
from calculus.enriched import constructors
from lib import library, common_vars
from lib.common_symbols import leftSymbol, rightSymbol, relationSymbol, domainSymbol
from lib.common_formulas import InDomain, Equal, IsEquivalence



x = common_vars.x()
def reflexive(e):
  return constructors.Forall([constructors.BoundedVariableBinding(x, e)],
      Equal(x, x, e))

x = common_vars.x()
y = common_vars.y()
def symmetric(e):
  return constructors.Forall([ constructors.BoundedVariableBinding(x, e)
                             , constructors.BoundedVariableBinding(y, e)],
      constructors.Implies(
        predicates = [Equal(x, y, e)],
        consequent = Equal(y, x, e)))

x = common_vars.x()
y = common_vars.y()
z = common_vars.z()
def transitive(e):
  return constructors.Forall([ constructors.BoundedVariableBinding(x, e)
                             , constructors.BoundedVariableBinding(y, e)
                             , constructors.BoundedVariableBinding(z, e)],
      constructors.Implies(
        predicates = [ Equal(x, y, e)
                     , Equal(y, z, e) ],
        consequent = Equal(x, z, e)))

A = common_vars.A()
claim = constructors.Forall([constructors.OrdinaryVariableBinding(A)],

    constructors.Iff(