| vout |
|---|
Pr9RN../8aa8f.. 1.02 barsTMUWB../1b679.. ownership of d4066.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMREM../7d2e4.. ownership of e7c7e.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMWFc../bb5fb.. ownership of e0bf3.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMNtk../b65ac.. ownership of d72c0.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMQsd../bb017.. ownership of 1267d.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMdZv../0fd8b.. ownership of 3c454.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMd1K../6f73a.. ownership of 2f0fc.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TML6C../94544.. ownership of abadb.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMM33../4570e.. ownership of 95448.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMJSz../b9a5e.. ownership of 22d9a.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMMey../76565.. ownership of 8ef0f.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMUC9../ba246.. ownership of 0bee3.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMQ9Y../7625a.. ownership of 38647.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMNxZ../b4baf.. ownership of 719d7.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TML7g../40bcd.. ownership of f325d.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMXpL../5b598.. ownership of 3276f.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMRtb../e18a8.. ownership of 9759f.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMWHP../35218.. ownership of ce5e0.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMGML../b7c8b.. ownership of 13d61.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMHyp../4fb61.. ownership of 3c1f1.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMJUp../b0278.. ownership of 429de.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0TMKwk../e18b4.. ownership of c75c4.. as prop with payaddr Pr3KZ.. rights free controlledby Pr3KZ.. upto 0PUb98../49060.. doc published by Pr3KZ..Param 2f869.. : (ι → ι → ο) → ι → ι → ι → ι → οDefinition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseDefinition 5a3b5.. := λ 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) ⟶ not (x0 x4 x5) ⟶ x6) ⟶ x6Definition 247da.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (5a3b5.. 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) ⟶ not (x0 x3 x6) ⟶ not (x0 x4 x6) ⟶ x0 x5 x6 ⟶ x7) ⟶ x7Param e643b.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → οParam 86706.. : ι → (ι → ι → ο) → οParam 35fb6.. : ι → (ι → ι → ο) → οKnown 1e947.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ 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 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ (x0 x3 x9 ⟶ x0 x3 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ x0 x3 x13 ⟶ x0 x3 x15 ⟶ FalseKnown 7f382.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ 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 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ (x0 x3 x9 ⟶ x0 x3 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ x0 x3 x13 ⟶ not (x0 x3 x15) ⟶ x0 x3 x14 ⟶ FalseKnown dcb1a.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ 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 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ (x0 x3 x9 ⟶ x0 x3 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ x0 x3 x13 ⟶ not (x0 x3 x15) ⟶ not (x0 x3 x14) ⟶ FalseKnown 60237.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ 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 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ (x0 x3 x9 ⟶ x0 x3 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ not (x0 x3 x13) ⟶ FalseDefinition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2Known xmxm : ∀ x0 : ο . or x0 (not x0)Theorem 429de.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ 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 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x8 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ (x0 x3 x9 ⟶ x0 x3 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ False...
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2Known dnegdneg : ∀ x0 : ο . not (not x0) ⟶ x0Known 636a9.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x6 x8 x4 x9 x2 x7 x3 x5Known andIandI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1Theorem 13d61.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x11 ⟶ not (x0 x3 x9) ⟶ False) ⟶ (x0 x2 x14 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x12 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x5 x10 ⟶ x0 x3 x13 ⟶ not (x0 x4 x10) ⟶ False) ⟶ False...
Known 66a94.. : ∀ 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 ⟶ 5a3b5.. x1 x2 x3 x4 x5 x6 ⟶ 5a3b5.. x1 x2 x3 x5 x4 x6Theorem 9759f.. : ∀ 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 ⟶ 247da.. x1 x2 x3 x4 x5 x6 x7 ⟶ 247da.. x1 x2 x3 x5 x4 x6 x7...
Theorem f325d.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x14 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x12 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x10 ⟶ not (x0 x3 x13) ⟶ False) ⟶ (x0 x2 x11 ⟶ not (x0 x3 x9) ⟶ False) ⟶ False...
Known 33ada.. : ∀ 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 ⟶ 2f869.. x1 x2 x3 x4 x5 ⟶ 2f869.. x1 x3 x2 x5 x4Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1 ⟶ ∀ x2 : ο . x2) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2Theorem 38647.. : ∀ 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 ⟶ 247da.. x1 x2 x3 x4 x5 x6 x7 ⟶ 247da.. x1 x3 x2 x5 x4 x7 x6...
Known 174e8.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x5 x3 x7 x2 x9 x4 x8 x6Known cc783.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x7 x5 x9 x3 x8 x2 x6 x4Theorem 8ef0f.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x3 x5 x2 x7 x4 x9 x6 x8...
Theorem 95448.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x3 x12 ⟶ not (x0 x2 x15) ⟶ False) ⟶ (x0 x3 x10 ⟶ not (x0 x2 x15) ⟶ False) ⟶ (x0 x3 x8 ⟶ not (x0 x2 x15) ⟶ False) ⟶ False...
Known f8e2e.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x3 x2 x5 x4 x7 x6 x9 x8Theorem 2f0fc.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x13 ⟶ not (x0 x3 x14) ⟶ False) ⟶ (x0 x2 x11 ⟶ not (x0 x3 x14) ⟶ False) ⟶ (x0 x2 x9 ⟶ not (x0 x3 x14) ⟶ False) ⟶ False...
Known 42c8f.. : ∀ 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 ⟶ e643b.. x1 x2 x3 x4 x5 x6 x7 x8 x9 ⟶ e643b.. x1 x2 x4 x3 x6 x5 x8 x7 x9Theorem 1267d.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x3 x12 ⟶ not (x0 x2 x13) ⟶ False) ⟶ (x0 x3 x10 ⟶ not (x0 x2 x13) ⟶ False) ⟶ False...
Theorem e0bf3.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ (x0 x2 x11 ⟶ not (x0 x3 x12) ⟶ False) ⟶ False...
Theorem d4066.. : ∀ 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) ⟶ 247da.. x0 x2 x3 x4 x5 x6 x7 ⟶ e643b.. (λ x16 x17 . not (x0 x16 x17)) x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False...
|
|