Search for blocks/addresses/...

Proofgold Term Root Disambiguation

hf term
(object) array( 'type' => 'termroot', 'hfbuiltin' => true, 'trmpres' => 'Loop_with_defs_cex2 = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (Loop_with_defs x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) (∀ x15 : ο . (∀ x16 . and (In x16 x1) (∀ x17 : ο . (∀ x18 . and (In x18 x1) (∀ x19 : ο . (∀ x20 . and (In x20 x1) (∀ x21 : ο . (∀ x22 . and (In x22 x1) (∀ x23 : ο . (∀ x24 . and (In x24 x1) (not (x7 x24 (x2 (x4 x5 x16) (x10 x18 x20 x16)) x22 = x5))x23)x23)x21)x21)x19)x19)x17)x17)x15)x15)', )
address
TMKpS..Loop_with_defs_cex2_def