• Ultra-Formal Verification of a Result in a System of Combinatory Logic

• General procedure used

• Notations and Definitions

• OTTER settings
  • Emergency measures

• Reflexive property of equality

• TRC Basic Axioms

• The term isp1 is a projection from functions to characteristic functions.
  • Definition of isp1
  • Basic defining properties of isp1
  • The combinator isp1 is a projection from functions to characteristic functions.

• The term notp1 finds complements of characteristic functions.
  • Definition of notp1
  • Basic defining clauses
  • Two simple properties
  • Algebra of notp1 and isp1 under composition

• The term charq is the characteristic function of the set of characteristic functions.
  • Definition of charq

• The term setof finds the characteristic function of a given function.
  • Definition of setof
  • Basic defining clauses (2 versions)
    • Defining clauses for setof using pair
    • Defining clauses for setof using p1 and p2.
  • Important properties of setof

• The term closedunder tests whether a set is closed under a function.
  • Definition of closedunder
  • Basic defining properties of closedunder

• Interlude 1: Some lemmas needed for intersections

• The combinator kintersection takes a set of sets, and returns a constant function whose value is the intersection.
  • Definition of kintersection

• The term subset tests the subset relationship between a given pair of characteristic functions.
  • Definition of subset
  • Basic defining properties of subset
  • Alternate version of defining properties for subset, using projections instead of pairs

• Interlude 2: some lemmas about kintersection, closedunder, and subset.

• The term closure finds the closure of a set under a function.
  • Definition of closure
  • Standard characterization of closure pair(s, f)
    • The set s is a subset of closure pair(s, f).
    • The set closure pair(s, f) is closed under f.
    • If x is a superset of s and is closed under f then closure pair(s, f) is a subset of x.
  • The term closure x is a characteristic function.
  • Standard characterization of closure reformulated using projections instead of pairing
    • The closure contains the set.
    • The closure is closed under the function.
    • The closure is the smallest such set.

• The term remove_singleton removes one element from a set.
  • Definition of remove_singleton
  • Basic defining properties of remove_singleton

• The term push is a bijection from the universe onto the characteristic functions.
  • Definition of push
  • Piecewise characterization of push
  • (push x) is a characteristic function
  • The function push always agrees with the identity function or with setof
  • push respects the partition of the universe by pushset, that is, pushset x = pushset (push x)
  • push is one-to-one
  • Lemmas on closure and remove_singleton
  • Lemmas on pushset
  • The function push is onto the characteristic functions