Ultra-Formal Verification of a Result in a System of Combinatory Logic
Reflexive property of equality
The term isp1 is a projection from functions to characteristic functions.
The term notp1 finds complements of characteristic functions.
The term charq is the characteristic function of the set of characteristic functions.
The term setof finds the characteristic function of a given function.
The term closedunder tests whether a set is closed under a function.
Interlude 1: Some lemmas needed for intersections
The term subset tests the subset relationship between a given pair of characteristic functions.
Interlude 2: some lemmas about kintersection, closedunder, and subset.
The term closure finds the closure of a set under a function.
The term remove_singleton removes one element from a set.
The term push is a bijection from the universe onto the characteristic functions.