| vout |
|---|
PrD6D../f5509.. 25.00 barsTMFNj../a7df8.. ownership of 9c595.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0TMdc1../c124d.. ownership of 31216.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0PUg1C../de927.. doc published by PrGM6..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseDefinition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2Known xmxm : ∀ x0 : ο . or x0 (not x0)Known dnegdneg : ∀ x0 : ο . not (not x0) ⟶ x0Theorem 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...
|
|