| vout |
|---|
PrPhD../d4632.. 3.41 barsTMdJS../7cf5d.. ownership of 5303f.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0TMQH2../fe3d0.. ownership of 3ef18.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0PUd7a../6d028.. doc published by PrPhD..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseTheorem 5303f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 x7 x8 : ι → ι → ι → ι . ∀ x9 x10 x11 x12 . ∀ x13 x14 : ι → ι → ι → ι → ι . ∀ x15 : ι → ι . ∀ x16 x17 . ∀ x18 : ι → ο . (∀ x19 x20 . x18 x20 ⟶ (x20 = x19 ⟶ False) ⟶ x18 x19 ⟶ False) ⟶ (∀ x19 x20 . x0 x19 x20 ⟶ x18 x20 ⟶ False) ⟶ (∀ x19 . x18 x19 ⟶ (x19 = x17 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x1 x20 x22 = x1 x19 x21 ⟶ (x22 = x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x1 x22 x20 = x1 x21 x19 ⟶ (x22 = x21 ⟶ False) ⟶ False) ⟶ (x18 x2 ⟶ False) ⟶ ((x18 x16 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . x18 (x3 x19 x20) ⟶ False) ⟶ (∀ x19 . x18 (x15 x19) ⟶ False) ⟶ (∀ x19 x20 . x18 (x1 x19 x20) ⟶ False) ⟶ ((x18 x17 ⟶ False) ⟶ False) ⟶ ((x18 x4 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . (x1 x20 x19 = x3 (x3 x20 x19) (x15 x20) ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x6 x19 x20 x21 = x1 (x8 x19 x20 x21) (x7 x19 x20 x21) ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x0 (x7 x19 x20 x21) x20 ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x0 (x8 x19 x20 x21) x21 ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 x23 . x0 (x6 x23 x21 x22) x23 ⟶ x0 x19 x22 ⟶ x0 x20 x21 ⟶ x6 x23 x21 x22 = x1 x19 x20 ⟶ (x23 = x5 x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 x23 x24 . x24 = x5 x22 x23 ⟶ x0 x19 x22 ⟶ x0 x21 x23 ⟶ x20 = x1 x19 x21 ⟶ (x0 x20 x24 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x19 = x1 (x13 x19 x22 x21 x20) (x14 x19 x22 x21 x20) ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x0 (x14 x19 x22 x21 x20) x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x0 (x13 x19 x22 x21 x20) x20 ⟶ False) ⟶ False) ⟶ ((x17 = x4 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . (x3 x20 x19 = x3 x19 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . x0 x19 x20 ⟶ x0 x20 x19 ⟶ False) ⟶ ((x0 x10 x9 ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ False) ⟶ False) ⟶ ((x0 x12 x11 ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ False) ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ x0 x12 x11 ⟶ x0 x10 x9 ⟶ False) ⟶ False (proof) |
|