# 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/natural.py
# S = common_vars.S
# def Natural(n):
# def Successor(a, b):
# def Less(a, b):
# def ForallNatural(variables, value):
# def ExistsNatural(variables, value):
# 
# 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/equivalence.py
# def reflexive(e):
# def symmetric(e):
# def transitive(e):
# A = common_vars.A()
# 
# Path: lib/function.py
# def projectSrc(f):
# def projectTgt(f):
# def projectDomain(e):
# def projectRelation(e):
# def defined(f):
# def wellDefined(f):
# def unique(f):
# A = common_vars.A()


from calculus.enriched import constructors
from lib import natural, library, common_vars, equivalence, function
# Copyright (C) 2013 Korei Klein <korei.klein1@gmail.com>


# A proof that forall n : N . S (S n) > n
n = common_vars.n()

a = common_vars.a()
b = common_vars.b()

claim = natural.Less(natural.zero,

# 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/natural.py
# S = common_vars.S
# def Natural(n):
# def Successor(a, b):
# def Less(a, b):
# def ForallNatural(variables, value):
# def ExistsNatural(variables, value):
# 
# 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/equivalence.py
# def reflexive(e):
# def symmetric(e):
# def transitive(e):
# A = common_vars.A()
# 
# Path: lib/function.py
# def projectSrc(f):
# def projectTgt(f):
# def projectDomain(e):
# def projectRelation(e):
# def defined(f):
# def wellDefined(f):
# def unique(f):
# A = common_vars.A()


# Path: examples/SS.py
from calculus.enriched import constructors
from lib import natural, library, common_vars, equivalence, function

# Copyright (C) 2013 Korei Klein <korei.klein1@gmail.com>


# A proof that forall n : N . S (S n) > n
n = common_vars.n()

a = common_vars.a()
b = common_vars.b()

claim = natural.Less(natural.zero,

    constructors.Apply( constructors.Apply(natural.zero, natural.S)