Proofgold Address

Known 7675c..^{combinator_def} : combinator = λ x1 . ∀ x2 : ι → ο . x2 (Inj0 0) ⟶ x2 (Inj0 (Power 0)) ⟶ (∀ x3 x4 . x2 x3 ⟶ x2 x4 ⟶ x2 (Inj1 (setsum x3 x4))) ⟶ x2 x1
Theorem d1f59..^combinator_K : combinator (Inj0 0) (proof)
Theorem d55a8..^combinator_S : combinator (Inj0 (Power 0)) (proof)
Theorem 8b007..^{combinator_Ap} : ∀ x0 x1 . combinator x0 ⟶ combinator x1 ⟶ combinator (Inj1 (setsum x0 x1)) (proof)
Known eb789..^andER : ∀ x0 x1 : ο . and x0 x1 ⟶ x1
Known 7c02f..^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known andE^andE : ∀ x0 x1 : ο . and x0 x1 ⟶ ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Theorem 69124..^{combinator_ind} : ∀ x0 : ι → ο . x0 (Inj0 0) ⟶ x0 (Inj0 (Power 0)) ⟶ (∀ x1 x2 . combinator x1 ⟶ x0 x1 ⟶ combinator x2 ⟶ x0 x2 ⟶ x0 (Inj1 (setsum x1 x2))) ⟶ ∀ x1 . combinator x1 ⟶ x0 x1 (proof)
Known b650a..^{combinator_equiv_def} : combinator_equiv = λ x1 x2 . ∀ x3 : ι → ι → ο . per_i x3 ⟶ (∀ x4 . combinator x4 ⟶ x3 x4 x4) ⟶ (∀ x4 x5 x6 x7 . combinator x4 ⟶ combinator x5 ⟶ combinator x6 ⟶ combinator x7 ⟶ x3 x4 x6 ⟶ x3 x5 x7 ⟶ x3 (Inj1 (setsum x4 x5)) (Inj1 (setsum x6 x7))) ⟶ (∀ x4 x5 . x3 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x4)) x5)) x4) ⟶ (∀ x4 x5 x6 . x3 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x4)) x5)) x6)) (Inj1 (setsum (Inj1 (setsum x4 x6)) (Inj1 (setsum x5 x6))))) ⟶ x3 x1 x2
Known 14d50..^per_i_E : ∀ x0 : ι → ι → ο . per_i x0 ⟶ ∀ x1 : ο . (symmetric_i x0 ⟶ transitive_i x0 ⟶ x1) ⟶ x1
Known 2acec..^{symmetric_i_E} : ∀ x0 : ι → ι → ο . symmetric_i x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1
Theorem be428..^{combinator_equiv_sym} : ∀ x0 x1 . combinator_equiv x0 x1 ⟶ combinator_equiv x1 x0 (proof)
Known 01483..^{transitive_i_E} : ∀ x0 : ι → ι → ο . transitive_i x0 ⟶ ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Theorem d25f0..^{combinator_equiv_tra} : ∀ x0 x1 x2 . combinator_equiv x0 x1 ⟶ combinator_equiv x1 x2 ⟶ combinator_equiv x0 x2 (proof)
Theorem b8d29..^{combinator_equiv_Ap} : ∀ x0 x1 x2 x3 . combinator x0 ⟶ combinator x1 ⟶ combinator x2 ⟶ combinator x3 ⟶ combinator_equiv x0 x2 ⟶ combinator_equiv x1 x3 ⟶ combinator_equiv (Inj1 (setsum x0 x1)) (Inj1 (setsum x2 x3)) (proof)
Theorem 80453..^{combinator_equiv_K} : ∀ x0 x1 . combinator_equiv (Inj1 (setsum (Inj1 (setsum (Inj0 0) x0)) x1)) x0 (proof)
Theorem 9464f..^{combinator_equiv_S} : ∀ x0 x1 x2 . combinator_equiv (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x0)) x1)) x2)) (Inj1 (setsum (Inj1 (setsum x0 x2)) (Inj1 (setsum x1 x2)))) (proof)
Theorem 474a0..^{combinator_equiv_ref} : ∀ x0 . combinator_equiv x0 x0 (proof)
Known 7c1a4..^per_i_I : ∀ x0 : ι → ι → ο . symmetric_i x0 ⟶ transitive_i x0 ⟶ per_i x0
Known c3f98..^{symmetric_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ symmetric_i x0
Known 11ad5..^{transitive_i_I} : ∀ x0 : ι → ι → ο . (∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3) ⟶ transitive_i x0
Theorem 28603..^{combinator_equiv_ind} : ∀ x0 : ι → ι → ο . per_i x0 ⟶ (∀ x1 . combinator x1 ⟶ x0 x1 x1) ⟶ (∀ x1 x2 x3 x4 . combinator x1 ⟶ combinator x2 ⟶ combinator x3 ⟶ combinator x4 ⟶ combinator_equiv x1 x3 ⟶ x0 x1 x3 ⟶ combinator_equiv x2 x4 ⟶ x0 x2 x4 ⟶ x0 (Inj1 (setsum x1 x2)) (Inj1 (setsum x3 x4))) ⟶ (∀ x1 x2 . x0 (Inj1 (setsum (Inj1 (setsum (Inj0 0) x1)) x2)) x1) ⟶ (∀ x1 x2 x3 . x0 (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) x1)) x2)) x3)) (Inj1 (setsum (Inj1 (setsum x1 x3)) (Inj1 (setsum x2 x3))))) ⟶ ∀ x1 x2 . combinator_equiv x1 x2 ⟶ x0 x1 x2 (proof)
Theorem 2992b..^{combinator_SKK} : ∀ x0 . combinator_equiv (Inj1 (setsum (Inj1 (setsum (Inj1 (setsum (Inj0 (Power 0)) (Inj0 0))) (Inj0 0))) x0)) x0 (proof)