Search for blocks/addresses/...
Proofgold Proposition
∀ 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 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
SNo
x4
⟶
SNo
x5
⟶
SNo
x6
⟶
SNo
x7
⟶
SNo
x8
⟶
SNo
x9
⟶
SNo
x10
⟶
SNo
x11
⟶
SNo
x12
⟶
SNo
x13
⟶
SNo
x14
⟶
SNo
x15
⟶
SNo
x16
⟶
SNo
x17
⟶
SNo
x18
⟶
SNo
x19
⟶
SNo
x20
⟶
SNo
x21
⟶
SNo
x22
⟶
SNo
x23
⟶
SNo
x24
⟶
SNo
x25
⟶
SNo
x26
⟶
SNo
x27
⟶
SNo
x28
⟶
SNo
x29
⟶
SNo
x30
⟶
SNo
x31
⟶
SNo
x32
⟶
SNo
x33
⟶
SNo
x34
⟶
SNo
x35
⟶
SNoLt
(
add_SNo
x18
(
add_SNo
x19
(
add_SNo
x20
(
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
x35
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
0
⟶
SNoLe
(
add_SNo
x1
(
minus_SNo
x0
)
)
x18
⟶
SNoLe
(
add_SNo
x2
(
minus_SNo
x1
)
)
x19
⟶
SNoLe
(
add_SNo
x3
(
minus_SNo
x2
)
)
x20
⟶
SNoLe
(
add_SNo
x4
(
minus_SNo
x3
)
)
x21
⟶
SNoLe
(
add_SNo
x5
(
minus_SNo
x4
)
)
x22
⟶
SNoLe
(
add_SNo
x6
(
minus_SNo
x5
)
)
x23
⟶
SNoLe
(
add_SNo
x7
(
minus_SNo
x6
)
)
x24
⟶
SNoLe
(
add_SNo
x8
(
minus_SNo
x7
)
)
x25
⟶
SNoLe
(
add_SNo
x9
(
minus_SNo
x8
)
)
x26
⟶
SNoLe
(
add_SNo
x10
(
minus_SNo
x9
)
)
x27
⟶
SNoLe
(
add_SNo
x11
(
minus_SNo
x10
)
)
x28
⟶
SNoLe
(
add_SNo
x12
(
minus_SNo
x11
)
)
x29
⟶
SNoLe
(
add_SNo
x13
(
minus_SNo
x12
)
)
x30
⟶
SNoLe
(
add_SNo
x14
(
minus_SNo
x13
)
)
x31
⟶
SNoLe
(
add_SNo
x15
(
minus_SNo
x14
)
)
x32
⟶
SNoLe
(
add_SNo
x16
(
minus_SNo
x15
)
)
x33
⟶
SNoLe
(
add_SNo
x17
(
minus_SNo
x16
)
)
x34
⟶
SNoLe
(
add_SNo
x0
(
minus_SNo
x17
)
)
x35
⟶
False
type
prop
theory
HotG
name
idl_negcycle_18
proof
PUU9h..
Megalodon
idl_negcycle_18
proofgold address
TMbTv..
idl_negcycle_18
creator
16810
PrGxv..
/
95607..
owner
16810
PrGxv..
/
95607..
term root
75a36..