Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition 2f869.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x1 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x2 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ not (x0 x2 x3) ⟶ not (x0 x1 x4) ⟶ not (x0 x2 x4) ⟶ x0 x3 x4 ⟶ x5) ⟶ x5
Definition 87c36.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. x0 x1 x2 x3 x4 ⟶ (x1 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x2 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x3 = x5 ⟶ ∀ x7 : ο . x7) ⟶ (x4 = x5 ⟶ ∀ x7 : ο . x7) ⟶ not (x0 x1 x5) ⟶ x0 x2 x5 ⟶ not (x0 x3 x5) ⟶ x0 x4 x5 ⟶ x6) ⟶ x6
Definition f201d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ x0 x1 x6 ⟶ not (x0 x2 x6) ⟶ x0 x3 x6 ⟶ not (x0 x4 x6) ⟶ x0 x5 x6 ⟶ x7) ⟶ x7
Definition 6648a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. x0 x1 x2 x3 x4 x5 ⟶ (x1 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x2 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x3 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x4 = x6 ⟶ ∀ x8 : ο . x8) ⟶ (x5 = x6 ⟶ ∀ x8 : ο . x8) ⟶ not (x0 x1 x6) ⟶ x0 x2 x6 ⟶ x0 x3 x6 ⟶ not (x0 x4 x6) ⟶ not (x0 x5 x6) ⟶ x7) ⟶ x7
Definition 836ee.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. x0 x1 x2 x3 x4 x5 x6 ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ x0 x1 x7 ⟶ not (x0 x2 x7) ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ x0 x5 x7 ⟶ x0 x6 x7 ⟶ x8) ⟶ x8
Definition 89dbd.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (836ee.. x0 x1 x2 x3 x4 x5 x6 x7 ⟶ (x1 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x2 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x3 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x4 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x5 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x6 = x8 ⟶ ∀ x10 : ο . x10) ⟶ (x7 = x8 ⟶ ∀ x10 : ο . x10) ⟶ x0 x1 x8 ⟶ x0 x2 x8 ⟶ not (x0 x3 x8) ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param atleastp^atleastp : ι → ι → ο
Definition cdfa5.. := λ x0 x1 . λ x2 : ι → ι → ο . ∀ x3 . x3 ⊆ x1 ⟶ atleastp x0 x3 ⟶ not (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x2 x4 x5)
Param u4 : ι
Definition 86706.. := cdfa5.. u4
Definition 35fb6.. := λ x0 . λ x1 : ι → ι → ο . 86706.. x0 (λ x2 x3 . not (x1 x2 x3))
Param SetAdjoin^SetAdjoin : ι → ι → ι
Param UPair^UPair : ι → ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Param equip^equip : ι → ι → ο
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known 7204a.. : ∀ x0 x1 x2 x3 . (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ equip u4 (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3)
Known 58c12.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x0 x1 x4 ⟶ x0 x2 x3 ⟶ x0 x2 x4 ⟶ x0 x3 x4 ⟶ (∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ x0 x5 x6 ⟶ x0 x6 x5) ⟶ ∀ x5 . x5 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ ∀ x6 . x6 ∈ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x0 x5 x6
Known c88f0.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⊆ x0
Theorem d9eaf.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x8 ⟶ not (x0 x2 x10) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x2 x15) ⟶ False) ⟶ (x0 x2 x8 ⟶ x0 x3 x15 ⟶ not (x0 x3 x11) ⟶ False) ⟶ False
Known 6f045.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x9 x8 x5 x4 x7 x6 x3 x2
Theorem 7e0df.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x15 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x15 ⟶ not (x0 x2 x10) ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x3 x8 ⟶ not (x0 x3 x10) ⟶ False) ⟶ False
Known a4071.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x2 x3 x5 x4 x7 x6 x8 x9
Known 3cb06.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x4 x6 x2 x9 x3 x8 x7 x5
Theorem bc193.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x4 x6 x9 x2 x8 x3 x7 x5
Theorem fee2d.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x11 ⟶ x0 x3 x10 ⟶ not (x0 x3 x15) ⟶ False) ⟶ (x0 x2 x11 ⟶ not (x0 x2 x8) ⟶ False) ⟶ False
Known 99aa6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ f201d.. x1 x2 x3 x4 x5 x6 x7 ⟶ f201d.. x1 x3 x2 x5 x4 x7 x6
Theorem c551f.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x3 x15 ⟶ not (x0 x3 x10) ⟶ False) ⟶ False
Known e5dcb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x9 x8 x4 x5 x6 x7 x3 x2
Theorem 2cb02.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x8 ⟶ not (x0 x2 x10) ⟶ False) ⟶ False
Known eab56.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 89dbd.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ 89dbd.. x1 x5 x7 x2 x9 x3 x8 x6 x4
Theorem 43b05.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ∀ x6 . x6 ∈ x1 ⟶ ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ ∀ x10 . x10 ∈ x1 ⟶ ∀ x11 . x11 ∈ x1 ⟶ ∀ x12 . x12 ∈ x1 ⟶ ∀ x13 . x13 ∈ x1 ⟶ ∀ x14 . x14 ∈ x1 ⟶ ∀ x15 . x15 ∈ x1 ⟶ (∀ x16 . x16 ∈ x1 ⟶ ∀ x17 . x17 ∈ x1 ⟶ x0 x16 x17 ⟶ x0 x17 x16) ⟶ (x2 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x8 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x9 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x10 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x11 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x12 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x13 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x14 ⟶ ∀ x16 : ο . x16) ⟶ (x2 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x3 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x4 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x5 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x6 = x15 ⟶ ∀ x16 : ο . x16) ⟶ (x7 = x15 ⟶ ∀ x16 : ο . x16) ⟶ f201d.. x0 x2 x3 x4 x5 x6 x7 ⟶ 89dbd.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False