| vout |
|---|
PrS5Z../5855f.. 24.98 barsTMGns../a3b49.. ownership of cc92e.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0TMQBU../f2931.. ownership of 1c763.. as prop with payaddr PrDsC.. rights free controlledby PrDsC.. upto 0PUM3u../52856.. doc published by PrDsC..Definition FalseFalse := ∀ x0 : ο . x0Definition notnot := λ x0 : ο . x0 ⟶ FalseTheorem cc92e..t13_arytm_3 : ∀ x0 : ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 x4 x5 : ι → ο . ∀ x6 x7 x8 . ∀ x9 : ι → ι . ∀ x10 x11 x12 x13 x14 . ∀ x15 x16 : ι → ο . ∀ x17 x18 x19 : ι → ι → ι . ∀ x20 x21 : ι → ο . ∀ x22 : ι → ι → ο . ∀ x23 : ι → ι → ι → ι . ∀ x24 : ι → ι → ο . ∀ x25 . ∀ x26 : ι → ι → ι . (∀ x27 x28 x29 . (x28 = x26 x27 x29 ⟶ False) ⟶ x20 x29 ⟶ x20 x27 ⟶ x21 x29 ⟶ x21 x27 ⟶ x22 x29 x28 ⟶ x22 x27 x28 ⟶ x24 x28 x25 ⟶ x22 x28 (x23 x27 x29 x28) ⟶ False) ⟶ (∀ x27 x28 x29 . (x28 = x26 x27 x29 ⟶ False) ⟶ (x22 x27 (x23 x27 x29 x28) ⟶ False) ⟶ x20 x29 ⟶ x20 x27 ⟶ x21 x29 ⟶ x21 x27 ⟶ x22 x29 x28 ⟶ x22 x27 x28 ⟶ x24 x28 x25 ⟶ False) ⟶ (∀ x27 x28 x29 . (x28 = x26 x29 x27 ⟶ False) ⟶ (x22 x27 (x23 x29 x27 x28) ⟶ False) ⟶ x20 x29 ⟶ x20 x27 ⟶ x21 x29 ⟶ x21 x27 ⟶ x22 x29 x28 ⟶ x22 x27 x28 ⟶ x24 x28 x25 ⟶ False) ⟶ (∀ x27 x28 x29 . (x28 = x26 x27 x29 ⟶ False) ⟶ (x21 (x23 x27 x29 x28) ⟶ False) ⟶ x20 x29 ⟶ x20 x27 ⟶ x21 x29 ⟶ x21 x27 ⟶ x22 x29 x28 ⟶ x22 x27 x28 ⟶ x24 x28 x25 ⟶ False) ⟶ (∀ x27 x28 x29 . (x28 = x26 x27 x29 ⟶ False) ⟶ (x20 (x23 x27 x29 x28) ⟶ False) ⟶ x20 x29 ⟶ x20 x27 ⟶ x21 x29 ⟶ x21 x27 ⟶ x22 x29 x28 ⟶ x22 x27 x28 ⟶ x24 x28 x25 ⟶ False) ⟶ (∀ x27 x28 x29 x30 . (x22 x29 x30 ⟶ False) ⟶ x29 = x26 x28 x27 ⟶ x20 x27 ⟶ x20 x28 ⟶ x20 x30 ⟶ x21 x27 ⟶ x21 x28 ⟶ x21 x30 ⟶ x22 x27 x30 ⟶ x22 x28 x30 ⟶ x24 x29 x25 ⟶ False) ⟶ (∀ x27 x28 . (x22 x28 x27 ⟶ False) ⟶ x19 x28 (x18 x27 x28) = x27 ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 x29 . (x0 (x0 x27 x28) x29 = x0 x27 (x0 x28 x29) ⟶ False) ⟶ x20 x29 ⟶ x20 x28 ⟶ x20 x27 ⟶ False) ⟶ (∀ x27 x28 . (x22 (x26 x27 x28) (x19 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x19 x27 (x18 x28 x27) = x28 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ x22 x27 x28 ⟶ False) ⟶ (∀ x27 x28 x29 . (x22 x28 x29 ⟶ False) ⟶ x29 = x26 x28 x27 ⟶ x20 x27 ⟶ x20 x28 ⟶ x21 x27 ⟶ x21 x28 ⟶ x24 x29 x25 ⟶ False) ⟶ (∀ x27 x28 x29 . (x22 x28 x29 ⟶ False) ⟶ x29 = x26 x27 x28 ⟶ x20 x27 ⟶ x20 x28 ⟶ x21 x27 ⟶ x21 x28 ⟶ x24 x29 x25 ⟶ False) ⟶ (∀ x27 x28 . (x0 x28 (x17 x28 x27) = x27 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x22 x28 x27 ⟶ False) ⟶ (∀ x27 x28 x29 . (x28 = x29 ⟶ False) ⟶ (x27 = x1 ⟶ False) ⟶ x0 x28 x27 = x0 x29 x27 ⟶ x20 x29 ⟶ x20 x27 ⟶ x20 x28 ⟶ False) ⟶ (∀ x27 x28 . (x24 (x26 x27 x28) x25 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x17 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x22 x27 x28 ⟶ False) ⟶ (∀ x27 x28 x29 . (x22 x28 x29 ⟶ False) ⟶ x29 = x0 x28 x27 ⟶ x20 x28 ⟶ x20 x29 ⟶ x20 x27 ⟶ False) ⟶ (∀ x27 x28 . (x21 (x0 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x21 (x18 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x0 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x18 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x19 x27 x28) ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x19 x27 x28 = x0 x27 x28 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x26 x27 x28 = x26 x28 x27 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . (x19 x27 x28 = x19 x28 x27 ⟶ False) ⟶ x20 x28 ⟶ x20 x27 ⟶ x21 x28 ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 x28 . x2 x27 x28 ⟶ x2 x28 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x0 x28 x27) ⟶ False) ⟶ x20 x27 ⟶ x20 x28 ⟶ False) ⟶ (∀ x27 x28 . (x20 (x18 x28 x27) ⟶ False) ⟶ x20 x27 ⟶ x20 x28 ⟶ False) ⟶ (∀ x27 x28 . (x16 x28 ⟶ False) ⟶ (x2 x27 x28 ⟶ False) ⟶ x24 x27 x28 ⟶ False) ⟶ (∀ x27 x28 . (x24 x28 x27 ⟶ False) ⟶ x2 x28 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 x28 ⟶ False) ⟶ x20 x27 ⟶ x24 x28 x27 ⟶ False) ⟶ (∀ x27 x28 . (x20 x28 ⟶ False) ⟶ x20 x27 ⟶ x24 x28 x27 ⟶ False) ⟶ (∀ x27 x28 . x16 x28 ⟶ x2 x27 x28 ⟶ False) ⟶ (∀ x27 x28 . (x22 x28 x28 ⟶ False) ⟶ x20 x27 ⟶ x20 x28 ⟶ False) ⟶ (∀ x27 . (x21 x27 ⟶ False) ⟶ x24 x27 x25 ⟶ False) ⟶ (∀ x27 . (x20 x27 ⟶ False) ⟶ x3 x27 ⟶ x4 x27 ⟶ False) ⟶ (∀ x27 x28 . (x28 = x27 ⟶ False) ⟶ x16 x27 ⟶ x16 x28 ⟶ False) ⟶ (∀ x27 . (x5 x27 ⟶ False) ⟶ x16 x27 ⟶ False) ⟶ (∀ x27 . (x15 x27 ⟶ False) ⟶ x16 x27 ⟶ False) ⟶ (∀ x27 . (x4 x27 ⟶ False) ⟶ x20 x27 ⟶ False) ⟶ (∀ x27 . (x3 x27 ⟶ False) ⟶ x20 x27 ⟶ False) ⟶ (∀ x27 . (x21 x27 ⟶ False) ⟶ x16 x27 ⟶ False) ⟶ (∀ x27 . (x20 x27 ⟶ False) ⟶ x16 x27 ⟶ False) ⟶ (∀ x27 . (x20 x27 ⟶ False) ⟶ x21 x27 ⟶ False) ⟶ (∀ x27 . (x27 = x1 ⟶ False) ⟶ x16 x27 ⟶ False) ⟶ (x22 (x18 (x19 x6 x7) (x26 x6 x7)) x6 ⟶ False) ⟶ (x16 x14 ⟶ False) ⟶ (x16 x8 ⟶ False) ⟶ (x16 x13 ⟶ False) ⟶ (x16 x25 ⟶ False) ⟶ (x1 = x7 ⟶ False) ⟶ (∀ x27 . (x24 (x9 x27) x27 ⟶ False) ⟶ False) ⟶ ((x24 x1 x25 ⟶ False) ⟶ False) ⟶ ((x16 x10 ⟶ False) ⟶ False) ⟶ ((x16 x1 ⟶ False) ⟶ False) ⟶ ((x4 x13 ⟶ False) ⟶ False) ⟶ ((x3 x13 ⟶ False) ⟶ False) ⟶ ((x21 x14 ⟶ False) ⟶ False) ⟶ ((x21 x12 ⟶ False) ⟶ False) ⟶ ((x21 x6 ⟶ False) ⟶ False) ⟶ ((x21 x7 ⟶ False) ⟶ False) ⟶ ((x20 x13 ⟶ False) ⟶ False) ⟶ ((x20 x11 ⟶ False) ⟶ False) ⟶ ((x20 x6 ⟶ False) ⟶ False) ⟶ ((x20 x7 ⟶ False) ⟶ False) ⟶ ((x20 x25 ⟶ False) ⟶ False) ⟶ False (proof) |
|