Search for blocks/addresses/...

Proofgold Proof

pf
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.
Assume H0: Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13.
Assume H1: In x4 x0.
Let x14 of type ο be given.
Assume H2: ∀ x15 . ...∀ x16 . ...∀ x17 . ...∀ x18 . ...∀ x19 . ..........................................(∀ x20 . ...∀ x21 . In x21 x0∀ x22 . In x22 x0In (x9 x20 x21 x22) x0)(∀ x20 . In x20 x0∀ x21 . In x21 x0x10 x20 x21 = x1 x20 (x1 x21 (x2 x20 x4)))(∀ x20 . In x20 x0∀ x21 . In x21 x0In (x10 x20 x21) x0)(∀ x20 . In x20 x0∀ x21 . In x21 x0x12 x20 x21 = x1 (x2 x20 x21) (x2 (x2 x20 x4) x4))(∀ x20 . In x20 x0∀ x21 . In x21 x0In (x12 x20 x21) x0)(∀ x20 . In x20 x0∀ x21 . In x21 x0x11 x20 x21 = x1 (x1 (x3 x4 x20) x21) x20)(∀ x20 . In x20 x0∀ x21 . In x21 x0In (x11 x20 x21) x0)(∀ x20 . In x20 x0∀ x21 . In x21 x0x13 x20 x21 = x1 (x3 x4 (x3 x4 x20)) (x3 x21 x20))(∀ x20 . In x20 x0∀ x21 . In x21 x0In (x13 x20 x21) x0)(∀ x20 . In x20 x0x1 x4 x20 = x20)(∀ x20 . In x20 x0x1 x20 x4 = x20)(∀ x20 . In x20 x0∀ x21 . In x21 x0x2 x20 (x1 x20 x21) = x21)(∀ x20 . In x20 x0∀ x21 . In x21 x0x1 x20 (x2 x20 x21) = x21)(∀ x20 . In x20 x0∀ x21 . In x21 x0x3 (x1 x20 x21) x21 = x20)(∀ x20 . In x20 x0∀ x21 . In x21 x0x1 (x3 x20 x21) x21 = x20)x14.
...