Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)(∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3 = x1 x3 x2)∀ x2 : ο . ((∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0x1 x3 (x1 x4 x5) = x1 x5 (x1 x3 x4))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 (x1 x3 x4) (x1 x5 x6) = x1 (x1 x3 x5) (x1 x4 x6))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 x3 (x1 x4 (x1 x5 x6)) = x1 x6 (x1 x3 (x1 x4 x5)))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 x3 (x1 x4 (x1 x5 x6)) = x1 x5 (x1 x6 (x1 x3 x4)))x2)x2
as obj
-
as prop
40e44..AssocComm_identities
theory
HotG
stx
b2e5e..
address
TMGvd..AssocComm_identities