| vout |
|---|
PrRdY../caabe.. 12.45 barsTMLsy../b7dde.. ownership of 420f0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0TMVgG../7c2c2.. ownership of 3cf9c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0PUdb4../3f290.. doc published by Pr4zB..Param 85e71.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → οParam notnot : ο → οDefinition 843b8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (85e71.. 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 ⟶ x0 x3 x7 ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8Known 89569.. : ∀ 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 ⟶ 85e71.. x1 x2 x3 x4 x5 x6 x7 ⟶ 85e71.. x1 x2 x3 x4 x6 x5 x7Theorem 420f0.. : ∀ 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 ⟶ 843b8.. x1 x2 x3 x4 x5 x6 x7 x8 ⟶ 843b8.. x1 x2 x3 x4 x6 x5 x7 x8 (proof) |
|