Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Let x0 of type ιιο be given.
Let x1 of type ιι be given.
Let x2 of type ιιο be given.
Let x3 of type ι be given.
Let x4 of type ιιι be given.
Let x5 of type ιιο be given.
Let x6 of type ιο be given.
Let x7 of type ιο be given.
Let x8 of type ιι be given.
Let x9 of type ιο be given.
Let x10 of type ιιι be given.
Let x11 of type ι be given.
Let x12 of type ιο be given.
Let x13 of type ιι be given.
Let x14 of type ιι be given.
Let x15 of type ιιι be given.
Let x16 of type ιιι be given.
Let x17 of type ι be given.
Let x18 of type ιο be given.
Let x19 of type ιο be given.
Let x20 of type ι be given.
Let x21 of type ιιο be given.
Let x22 of type ι be given.
Let x23 of type ι be given.
Let x24 of type ι be given.
Let x25 of type ι be given.
Let x26 of type ι be given.
Let x27 of type ι be given.
Let x28 of type ιιο be given.
Let x29 of type ι be given.
Let x30 of type ιι be given.
Let x31 of type ιιι be given.
Let x32 of type ι be given.
Let x33 of type ι be given.
Let x34 of type ιο be given.
Let x35 of type ιιο be given.
Let x36 of type ιι be given.
Let x37 of type ι be given.
Let x38 of type ιο be given.
Let x39 of type ιιο be given.
Let x40 of type ιιι be given.
Let x41 of type ι be given.
Let x42 of type ιο be given.
Let x43 of type ιιιιο be given.
Let x44 of type ιιιιιο be given.
Let x45 of type ιιι be given.
Let x46 of type ιιι be given.
Let x47 of type ιιιιιο be given.
Let x48 of type ιιο be given.
Let x49 of type ιο be given.
Let x50 of type ιι be given.
Let x51 of type ιιιο be given.
Let x52 of type ιιο be given.
Let x53 of type ιιιιο be given.
Let x54 of type ιιιιι be given.
Let x55 of type ιιι be given.
Let x56 of type ιιιο be given.
Let x57 of type ιο be given.
Let x58 of type ιο be given.
Let x59 of type ιο be given.
Let x60 of type ι be given.
Let x61 of type ιο be given.
Assume H5: ∀ x62 x63 . x61 x63(x63 = x62False)x61 x62False.
Assume H6: ∀ x62 x63 . x0 x62 x63x61 x63False.
Assume H7: ∀ x62 . x61 x62(x62 = x60False)False.
Assume H8: ∀ x62 x63 x64 . x0 x62 x63x2 x63 (x1 x64)x61 x64False.
Assume H9: ∀ x62 x63 x64 x65 x66 . (x59 x66False)x49 x66x58 x66x2 x62 (x50 x66)x2 x65 (x50 x66)x2 x63 (x50 x66)x57 x64x51 x64 (x50 x66) (x50 x66)x56 x64 (x50 x66) (x50 x66)x2 x64 (x1 (x55 (x50 x66) (x50 x66)))x52 x64 x66x54 (x50 x66) (x50 x66) x64 x62 = x62x53 x66 x65 x62 (x54 (x50 x66) (x50 x66) x64 x65)(x65 = x62False)(x53 x66 x63 x62 (x54 (x50 x66) (x50 x66) x64 x63)False)False.
Assume H10: ∀ x62 x63 x64 . x0 x63 x64x2 x64 (x1 x62)(x2 x63 x62False)False.
Assume H11: ∀ x62 x63 . x48 x63 x62(x2 x63 (x1 x62)False)False.
Assume H12: ∀ x62 x63 . x2 x63 (x1 x62)(x48 x63 x62False)False.
Assume H13: ∀ x62 x63 . (x59 x63False)x49 x63x58 x63x57 x62x51 x62 (x50 x63) (x50 x63)x56 x62 (x50 x63) (x50 x63)x2 x62 (x1 (x55 (x50 x63) (x50 x63)))x47 x63 (x46 x62 x63) (x45 x62 x63) (x54 (x50 x63) (x50 x63) x62 (x46 x62 x63)) (x54 (x50 x63) (x50 x63) x62 (x45 x62 x63))(x52 x62 x63False)False.
Assume H14: ∀ x62 x63 . ........................(x52 x62 ...False)False.
...