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 . SNo x0SNo x1SNo x2SNo x3SNo x4SNo x5SNo x6SNo x7SNo x8SNo x9SNo x10SNo x11SNo x12SNo x13SNo x14SNo x15SNo x16SNo x17SNo x18SNo x19SNo x20SNo x21SNo x22SNo x23SNo x24SNo x25SNo x26SNo x27SNo x28SNo x29SNo x30SNo x31SNo x32SNo x33SNo x34SNo x35SNo x36SNo x37SNo x38SNo x39SNo x40SNo x41SNoLt (add_SNo x21 (add_SNo x22 (add_SNo x23 (add_SNo x24 (add_SNo x25 (add_SNo x26 (add_SNo x27 (add_SNo x28 (add_SNo x29 (add_SNo x30 (add_SNo x31 (add_SNo x32 (add_SNo x33 (add_SNo x34 (add_SNo x35 (add_SNo x36 (add_SNo x37 (add_SNo x38 (add_SNo x39 (add_SNo x40 x41)))))))))))))))))))) 0SNoLe (add_SNo x1 (minus_SNo x0)) x21SNoLe (add_SNo x2 (minus_SNo x1)) x22SNoLe (add_SNo x3 (minus_SNo x2)) x23SNoLe (add_SNo x4 (minus_SNo x3)) x24SNoLe (add_SNo x5 (minus_SNo x4)) x25SNoLe (add_SNo x6 (minus_SNo x5)) x26SNoLe (add_SNo x7 (minus_SNo x6)) x27SNoLe (add_SNo x8 (minus_SNo x7)) x28SNoLe (add_SNo x9 (minus_SNo x8)) x29SNoLe (add_SNo x10 (minus_SNo x9)) x30SNoLe (add_SNo x11 (minus_SNo x10)) x31SNoLe (add_SNo x12 (minus_SNo x11)) x32SNoLe (add_SNo x13 (minus_SNo x12)) x33SNoLe (add_SNo x14 (minus_SNo x13)) x34SNoLe (add_SNo x15 (minus_SNo x14)) x35SNoLe (add_SNo x16 (minus_SNo x15)) x36SNoLe (add_SNo x17 (minus_SNo x16)) x37SNoLe (add_SNo x18 (minus_SNo x17)) x38SNoLe (add_SNo x19 (minus_SNo x18)) x39SNoLe (add_SNo x20 (minus_SNo x19)) x40SNoLe (add_SNo x0 (minus_SNo x20)) x41False
as obj
-
as prop
64193..idl_negcycle_21
theory
HotG
stx
27254..
address
TMQgf..idl_negcycle_21