Search for blocks/addresses/...

Proofgold Term Root Disambiguation

hf term
(object) array( 'type' => 'termroot', 'hfbuiltin' => true, 'trmpres' => 'Loop = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . and (and (and (and (binop_on x1 x2) (binop_on x1 x3)) (binop_on x1 x4)) (∀ x6 . In x6 x1and (x2 x5 x6 = x6) (x2 x6 x5 = x6))) (∀ x6 . In x6 x1∀ x7 . In x7 x1and (and (and (x3 x6 (x2 x6 x7) = x7) (x2 x6 (x3 x6 x7) = x7)) (x4 (x2 x6 x7) x7 = x6)) (x2 (x4 x6 x7) x7 = x6))', )
address
TMFcH..Loop_def