Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ 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 : ι → ι → ο . ∀ x30 x31 . ∀ x32 : ι → ο . ∀ x33 : ι → ι . ∀ x34 : ι → ο . ∀ x35 . ∀ x36 : ι → ι → ο . ∀ x37 : ι → ι . ∀ x38 : ι → ι → ο . ∀ x39 : ι → ο . ∀ x40 . ∀ x41 : ι → ι → ι . ∀ x42 : ι → ι . ∀ x43 : ι → ι → ι . ∀ x44 x45 : ι → ο . (∀ x46 x47 . x45 x47(x47 = x46False)x45 x46False)(∀ x46 x47 . x0 x46 x47x45 x47False)(∀ x46 x47 x48 x49 . x44 x49x44 x46x0 (x43 x48 x47) (x42 x46)(x0 (x43 x48 x47) (x42 (x41 x49 x46))False)False)(∀ x46 x47 x48 x49 . x44 x49x44 x46x0 (x43 x48 x47) (x42 x49)(x0 (x43 x48 x47) (x42 (x41 x49 x46))False)False)(∀ x46 . x45 x46(x46 = x40False)False)(∀ x46 x47 x48 . x0 x46 x47x2 x47 (x1 x48)x45 x48False)(∀ x46 x47 x48 x49 . x44 x49x44 x46x0 (x43 x48 x47) (x42 (x41 x49 x46))x0 x48 (x37 x46)x0 x47 (x37 x46)x38 x49 x46x39 x46(x0 (x43 x48 x47) (x42 x46)False)False)(∀ x46 x47 x48 . x0 x47 x48x2 x48 (x1 x46)(x2 x47 x46False)False)(∀ x46 x47 . x36 x47 x46(x2 x47 (x1 x46)False)False)(∀ x46 x47 . x2 x47 (x1 x46)(x36 x47 x46False)False)(∀ x46 x47 . x2 x46 x47(x45 x47False)(x0 x46 x47False)False)(∀ x46 x47 . x0 x47 x46(x2 x47 x46False)False)(x45 x35False)(∀ x46 . (x36 x46 x46False)False)(∀ x46 . (x34 x46False)x32 x46x45 (x33 x46)False)(∀ x46 . (x34 x46False)x32 x46(x2 (x33 x46) (x1 (x37 x46))False)False)(x45 x31False)(∀ x46 . (x3 x46False)x32 x46x4 (x5 x46)False)(∀ x46 . (x3 x46False)x32 x46(x2 (x5 x46) (x1 (x37 x46))False)False)(∀ x46 . (x34 x46False)x32 x46(x4 (x6 x46)False)False)(∀ x46 . (x34 x46False)x32 x46x45 (x6 x46)False)(∀ x46 . (x34 x46False)x32 x46(x2 (x6 x46) (x1 (x37 x46))False)False)((x45 x30False)False)(∀ x46 . x44 x46(x8 (x7 x46) x46False)False)(∀ x46 . x44 x46(x29 (x7 x46) x46False)False)(∀ x46 . x44 x46(x2 (x7 x46) (x1 (x37 x46))False)False)(∀ x46 x47 . (x28 (x27 x46 x47) x46False)False)(∀ x46 x47 . (x9 (x27 x47 x46) x46False)False)(∀ x46 x47 . (x26 (x27 x46 x47)False)False)(∀ x46 x47 . (x45 (x27 x46 x47)False)False)(∀ x46 x47 . (x2 (x27 x46 x47) (x1 (x25 x47 x46))False)False)(∀ x46 x47 x48 x49 . x2 x48 (x1 (x25 x49 x49))x10 x49 x48 = x10 x47 x46(x48 = x46False)False)(∀ x46 x47 x48 x49 . x2 x48 (x1 (x25 x49 x49))x10 x49 x48 = x10 x46 x47(x49 = x46False)False)(∀ x46 . (x11 x46False)x32 x46x12 (x37 x46)False)(∀ x46 . x11 x46x32 x46(x12 (x37 x46)False)False)(∀ x46 . x3 x46x32 x46(x4 (x37 x46)False)False)(∀ x46 . (x3 x46False)x32 x46x4 (x37 x46)False)(∀ x46 . (x34 x46False)x32 x46x45 (x37 x46)False)(∀ x46 x47 . (x34 x47False)x44 x47x44 x46(x24 (x41 x47 x46)False)False)(∀ x46 x47 . (x34 x47False)x44 x47x44 x46x34 (x41 x47 x46)False)((x45 x40False)False)(∀ x46 . x34 x46x32 x46(x45 (x37 x46)False)False)(∀ x46 x47 . x44 x47(x34 x46False)x44 x46(x24 (x41 x47 x46)False)False)(∀ x46 x47 . x44 x47(x34 x46False)x44 x46x34 (x41 x47 x46)False)(∀ x46 . (x2 (x23 x46) x46False)False)((x32 x13False)False)((x44 x22False)False)(∀ x46 . x44 x46(x2 (x42 x46) (x1 (x25 (x37 x46) (x37 x46)))False)False)(∀ x46 . x44 x46(x32 x46False)False)(∀ x46 x47 . x44 x47x44 x46(x44 (x41 x47 x46)False)False)(∀ x46 x47 . x44 x47x44 x46(x24 (x41 x47 x46)False)False)(∀ x46 x47 . x2 x47 (x1 (x25 x46 x46))(x44 (x10 x46 x47)False)False)(∀ x46 x47 . x2 x47 (x1 (x25 x46 x46))(x24 (x10 x46 x47)False)False)(∀ x46 x47 x48 . x44 x48x2 x46 (x37 x48)x2 x47 (x37 x48)x0 (x43 x46 x47) (x42 x48)(x14 x48 x46 x47False)False)(∀ x46 x47 x48 . x44 x48x2 x46 (x37 x48)x2 x47 (x37 x48)x14 x48 x46 x47(x0 (x43 x46 x47) (x42 x48)False)False)(∀ x46 . x32 x46x15 x46 x40(x34 x46False)False)(∀ x46 . x32 x46x34 x46(x15 x46 x40False)False)(∀ x46 . x32 x46(x11 x46False)x3 x46False)(∀ x46 . x32 x46x3 x46(x11 x46False)False)(∀ x46 . x32 x46(x11 x46False)x11 x46False)(∀ x46 . x32 x46(x11 x46False)x34 x46False)(∀ x46 . x32 x46x34 x46(x11 x46False)False)(∀ x46 . x32 x46x34 x46(x34 x46False)False)(∀ x46 x47 x48 . x45 x48x2 x46 (x1 (x25 x47 x48))(x45 x46False)False)(∀ x46 x47 x48 . x45 x48x2 x46 (x1 (x25 x48 x47))(x45 x46False)False)(∀ x46 . x32 x46(x3 x46False)x34 x46False)(∀ x46 x47 x48 . x2 x48 (x1 (x25 x46 x47))(x28 x48 x47False)False)(∀ x46 x47 x48 . x2 x48 (x1 (x25 x47 x46))(x9 x48 x47False)False)(∀ x46 x47 . x44 x47x2 x46 (x1 (x37 x47))x45 x46(x8 x46 x47False)False)(∀ x46 x47 . x44 x47x2 x46 (x1 (x37 x47))x45 x46(x29 x46 x47False)False)(∀ x46 . x32 x46x34 x46(x3 x46False)False)(∀ x46 x47 x48 . x2 x48 (x1 (x25 x46 x47))(x26 x48False)False)(∀ x46 . x32 x46(x3 x46False)x34 x46False)(∀ x46 . x32 x46x15 x46 x35(x3 x46False)False)(∀ x46 . x32 x46x15 x46 x35x34 x46False)(∀ x46 . x32 x46(x34 x46False)x3 x46(x15 x46 x35False)False)(∀ x46 x47 . x0 x46 x47x0 x47 x46False)(∀ x46 . x44 x46x24 x46(x46 = x10 (x37 x46) (x42 x46)False)False)((x14 x19 x20 x21False)(x14 (x41 x18 x19) x17 x16False)False)(x14 (x41 x18 x19) x17 x16x14 x19 x20 x21False)((x39 x19False)False)((x38 x18 x19False)False)((x16 = x21False)False)((x17 = x20False)False)((x2 x21 (x37 x19)False)False)((x2 x20 (x37 x19)False)False)((x2 x16 (x37 (x41 x18 x19))False)False)((x2 x17 (x37 (x41 x18 x19))False)False)((x44 x19False)False)(x34 x19False)((x44 x18False)False)(x34 x18False)False
as obj
-
as prop
99b52..
theory
HotG
stx
04bda..
address
TMSdZ..