Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrD6D../c542d..
PUZds../02ce1..
vout
PrD6D../ca675.. 24.90 bars
TMRQi../8e5e9.. ownership of aed72.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0
TMSCw../6f03c.. ownership of e1179.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0
TMHxZ../a6bfc.. ownership of bc9f8.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0
TMK5o../fed0c.. ownership of d24eb.. as prop with payaddr PrGM6.. rights free controlledby PrGM6.. upto 0
PUhfA../bfadb.. doc published by PrGM6..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Known pred_ext_2pred_ext_2 : ∀ x0 x1 : ι → ο . (∀ x2 . x0 x2 ⟶ x1 x2) ⟶ (∀ x2 . x1 x2 ⟶ x0 x2) ⟶ x0 = x1
Known dnegdneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem bc9f8.. : ∀ x0 : ι → ι → ο . (λ x2 x3 . not (not (x0 x2 x3))) = x0
...

Definition SubqSubq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param setminussetminus : ι → ι → ι
Param 00e19.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ο
Param atleastpatleastp : ι → ι → ο
Param u7 : ι
Param 4402e.. : ι → (ι → ι → ο) → ο
Definition 86ec2.. := λ x0 . λ x1 : ι → ι → ο . 4402e.. x0 (λ x2 x3 . not (x1 x2 x3))
Definition cdfa5.. := λ x0 x1 . λ x2 : ι → ι → ο . ∀ x3 . x3 ⊆ x1 ⟶ atleastp x0 x3 ⟶ not (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x2 x4 x5)
Param u4 : ι
Definition 86706.. := cdfa5.. u4
Definition 35fb6.. := λ x0 . λ x1 : ι → ι → ο . 86706.. x0 (λ x2 x3 . not (x1 x2 x3))
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition nInnIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ and (x2 ∈ x0) (nIn x2 x1)
Param 6648a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ο
Definition c9184.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. 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 ⟶ not (x0 x2 x7) ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ not (x0 x6 x7) ⟶ x8) ⟶ x8
Param e7595.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 88b7c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 81638.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 70d65.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 843b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Param 2452c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ο
Definition df271.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. 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 ⟶ not (x0 x2 x7) ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ not (x0 x5 x7) ⟶ x0 x6 x7 ⟶ x8) ⟶ x8
Definition 836ee.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. 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 ⟶ not (x0 x2 x7) ⟶ not (x0 x3 x7) ⟶ not (x0 x4 x7) ⟶ x0 x5 x7 ⟶ x0 x6 x7 ⟶ x8) ⟶ x8
Known e5914.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ atleastp u7 x0 ⟶ 4402e.. x0 x1 ⟶ 35fb6.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ c9184.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ e7595.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 88b7c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 81638.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 70d65.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 843b8.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 2452c.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ df271.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ 836ee.. x1 x3 x4 x5 x6 x7 x8 x9 ⟶ x2) ⟶ x2
Known 917b0.. : ∀ 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 ⟶ x0 x14 x15 ⟶ x0 x15 x14) ⟶ (x2 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x8 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x9 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x10 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x11 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x13 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x13 ⟶ ∀ x14 : ο . x14) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 6648a.. (λ x14 x15 . not (x0 x14 x15)) x8 x9 x10 x11 x12 x13 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known 1c304.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ e7595.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known 15c2f.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 88b7c.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known 1e702.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 81638.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known 06402.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 70d65.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known c62c7.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 843b8.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known 659aa.. : ∀ 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 ⟶ x0 x15 x16 ⟶ x0 x16 x15) ⟶ (x2 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x8 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x9 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x10 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x11 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x12 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x14 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x14 ⟶ ∀ x15 : ο . x15) ⟶ 00e19.. x0 x2 x3 x4 x5 x6 x7 ⟶ 2452c.. (λ x15 x16 . not (x0 x15 x16)) x8 x9 x10 x11 x12 x13 x14 ⟶ 86706.. x1 x0 ⟶ 35fb6.. x1 x0 ⟶ False
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem aed72.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x1 ⊆ x2 ⟶ ∀ x3 . x3 ∈ setminus x2 x1 ⟶ ∀ x4 . x4 ∈ setminus x2 x1 ⟶ ∀ x5 . x5 ∈ setminus x2 x1 ⟶ ∀ x6 . x6 ∈ setminus x2 x1 ⟶ ∀ x7 . x7 ∈ setminus x2 x1 ⟶ ∀ x8 . x8 ∈ setminus x2 x1 ⟶ (∀ x9 . x9 ∈ x2 ⟶ ∀ x10 . x10 ∈ x2 ⟶ x0 x9 x10 ⟶ x0 x10 x9) ⟶ 00e19.. x0 x3 x4 x5 x6 x7 x8 ⟶ atleastp u7 x1 ⟶ 86ec2.. x1 x0 ⟶ 86706.. x2 x0 ⟶ 35fb6.. x2 x0 ⟶ False
...