Proofgold Asset

Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param Sing^Sing : ι → ι
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Theorem 6cd03.. : ∀ x0 x1 . x1 ∈ x0 ⟶ Sing x1 ⊆ x0
Param UPair^UPair : ι → ι → ι
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known UPairE^UPairE : ∀ x0 x1 x2 . x0 ∈ UPair x1 x2 ⟶ or (x0 = x1) (x0 = x2)
Theorem f7dd2.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ UPair x1 x2 ⊆ x0
Param binunion^binunion : ι → ι → ι
Definition SetAdjoin^SetAdjoin := λ x0 x1 . binunion x0 (Sing x1)
Known binunion_Subq_min^{binunion_Subq_min} : ∀ x0 x1 x2 . x0 ⊆ x2 ⟶ x1 ⊆ x2 ⟶ binunion x0 x1 ⊆ x2
Theorem 6219b.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ SetAdjoin (UPair x1 x2) x3 ⊆ x0
Theorem c88f0.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ SetAdjoin (SetAdjoin (UPair x1 x2) x3) x4 ⊆ x0
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known binunionI1^binunionI1 : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ x2 ∈ binunion x0 x1
Known binunionI2^binunionI2 : ∀ x0 x1 x2 . x2 ∈ x1 ⟶ x2 ∈ binunion x0 x1
Known SingI^SingI : ∀ x0 . x0 ∈ Sing x0
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 65822.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ x0 x3 x2) ⟶ (∀ x3 . x3 ∈ binunion x1 (Sing x2) ⟶ ∀ x4 . x4 ∈ binunion x1 (Sing x2) ⟶ x0 x3 x4 ⟶ x0 x4 x3) ⟶ ∀ x3 . x3 ∈ binunion x1 (Sing x2) ⟶ ∀ x4 . x4 ∈ binunion x1 (Sing x2) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x0 x3 x4
Known UPairI1^UPairI1 : ∀ x0 x1 . x0 ∈ UPair x0 x1
Known UPairI2^UPairI2 : ∀ x0 x1 . x1 ∈ UPair x0 x1
Theorem c7e9c.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x0 x2 x3 ⟶ (∀ x4 . x4 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ x0 x4 x5 ⟶ x0 x5 x4) ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ ∀ x5 . x5 ∈ SetAdjoin (UPair x1 x2) x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x4 x5
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0 ⟶ x3 x1 ⟶ x3 x2 ⟶ ∀ x4 . x4 ∈ SetAdjoin (UPair x0 x1) x2 ⟶ x3 x4
Theorem 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
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 9c595.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . (x0 x6 x10 ⟶ x0 x1 x10 ⟶ x0 x6 x9 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x1 x11 ⟶ x0 x1 x10 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x2 x11 ⟶ x0 x2 x10 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x11 ⟶ x0 x4 x10 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x1 x12 ⟶ x0 x1 x10 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x6 x13 ⟶ x0 x1 x13 ⟶ x0 x6 x9 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x2 x13 ⟶ x0 x2 x11 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x13 ⟶ x0 x4 x11 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x3 x14 ⟶ x0 x4 x12 ⟶ x0 x3 x12 ⟶ False) ⟶ (x0 x2 x14 ⟶ x0 x2 x12 ⟶ x0 x2 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x4 x12 ⟶ x0 x4 x9 ⟶ False) ⟶ (x0 x4 x14 ⟶ x0 x3 x14 ⟶ x0 x4 x13 ⟶ x0 x3 x13 ⟶ False) ⟶ (x0 x1 x14 ⟶ x0 x1 x13 ⟶ x0 x1 x9 ⟶ False) ⟶ (x0 x6 x15 ⟶ x0 x1 x15 ⟶ x0 x6 x10 ⟶ x0 x1 x10 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x3 x15 ⟶ x0 x4 x11 ⟶ x0 x3 x11 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x11 ⟶ x0 x2 x11 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x11 ⟶ x0 x2 x10 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x11 ⟶ x0 x3 x10 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x11 ⟶ x0 x4 x10 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x12 ⟶ x0 x2 x12 ⟶ False) ⟶ (x0 x6 x15 ⟶ x0 x1 x15 ⟶ x0 x6 x13 ⟶ x0 x1 x13 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x13 ⟶ x0 x2 x11 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x13 ⟶ x0 x3 x11 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x13 ⟶ x0 x4 x11 ⟶ False) ⟶ (x0 x5 x15 ⟶ x0 x2 x15 ⟶ x0 x5 x14 ⟶ x0 x2 x14 ⟶ False) ⟶ (x0 x2 x15 ⟶ x0 x2 x14 ⟶ x0 x2 x12 ⟶ False) ⟶ (x0 x3 x15 ⟶ x0 x3 x14 ⟶ x0 x3 x12 ⟶ False) ⟶ (x0 x4 x15 ⟶ x0 x4 x14 ⟶ x0 x4 x12 ⟶ False) ⟶ (not (x0 x3 x9) ⟶ not (x0 x2 x9) ⟶ not (x0 x1 x9) ⟶ False) ⟶ (not (x0 x3 x12) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x4 x12) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x2 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x3 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x4 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x5 x12) ⟶ not (x0 x1 x12) ⟶ not (x0 x5 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ False) ⟶ (not (x0 x4 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ False) ⟶ (not (x0 x3 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x3 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x4 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x4 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x6 x13) ⟶ not (x0 x2 x13) ⟶ not (x0 x6 x10) ⟶ not (x0 x2 x10) ⟶ False) ⟶ (not (x0 x2 x13) ⟶ not (x0 x1 x13) ⟶ not (x0 x2 x12) ⟶ not (x0 x1 x12) ⟶ False) ⟶ (not (x0 x3 x14) ⟶ not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ False) ⟶ (not (x0 x4 x14) ⟶ not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ False) ⟶ (not (x0 x2 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x2 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x3 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x3 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x4 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x5 x14) ⟶ not (x0 x1 x14) ⟶ not (x0 x5 x11) ⟶ not (x0 x1 x11) ⟶ False) ⟶ (not (x0 x4 x15) ⟶ not (x0 x2 x15) ⟶ not (x0 x1 x15) ⟶ False) ⟶ (not (x0 x5 x15) ⟶ not (x0 x3 x15) ⟶ not (x0 x1 x15) ⟶ False) ⟶ (not (x0 x3 x15) ⟶ not (x0 x2 x15) ⟶ not (x0 x3 x9) ⟶ not (x0 x2 x9) ⟶ False) ⟶ (not (x0 x6 x15) ⟶ not (x0 x4 x15) ⟶ not (x0 x6 x9) ⟶ not (x0 x4 x9) ⟶ False) ⟶ (x0 x1 x11 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x1 x12 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x1 x13 ⟶ not (x0 x1 x10) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x1 x9) ⟶ False) ⟶ (x0 x3 x9 ⟶ not (x0 x2 x9) ⟶ False) ⟶ (not (x0 x1 x11) ⟶ not (x0 x1 x12) ⟶ x0 x1 x14 ⟶ not (x0 x1 x13) ⟶ False) ⟶ (x0 x1 x9 ⟶ x0 x1 x15 ⟶ x0 x3 x15 ⟶ not (x0 x2 x9) ⟶ False) ⟶ 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 2452c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f201d.. 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 ⟶ x0 x2 x7 ⟶ not (x0 x3 x7) ⟶ x0 x4 x7 ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Definition e643b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (2452c.. 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 ⟶ x0 x3 x8 ⟶ not (x0 x4 x8) ⟶ not (x0 x5 x8) ⟶ not (x0 x6 x8) ⟶ not (x0 x7 x8) ⟶ x9) ⟶ x9
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 c9184.. := λ 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) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
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 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 dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 38317.. : ∀ 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 ⟶ ∀ x18 . x18 ∈ x1 ⟶ x0 x17 x18 ⟶ x0 x18 x17) ⟶ (x2 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x10 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x11 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x12 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x13 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x14 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x15 ⟶ ∀ x17 : ο . x17) ⟶ (x2 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x3 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x4 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x5 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x6 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x7 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x8 = x16 ⟶ ∀ x17 : ο . x17) ⟶ (x9 = x16 ⟶ ∀ x17 : ο . x17) ⟶ e643b.. x0 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ c9184.. (λ x17 x18 . not (x0 x17 x18)) x10 x11 x12 x13 x14 x15 x16 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x12 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x13 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x2 x14 ⟶ not (x0 x2 x11) ⟶ False) ⟶ (x0 x3 x10 ⟶ not (x0 x2 x10) ⟶ False) ⟶ (x0 x4 x10 ⟶ not (x0 x3 x10) ⟶ False) ⟶ (not (x0 x2 x12) ⟶ not (x0 x2 x13) ⟶ x0 x2 x15 ⟶ not (x0 x2 x14) ⟶ False) ⟶ (x0 x2 x10 ⟶ x0 x2 x16 ⟶ x0 x4 x16 ⟶ not (x0 x3 x10) ⟶ False) ⟶ False