load modules/pichler.maude --- Pulled from Ex. 3.6 in Pichler's paper: --- "Explicit Vs. Implicit Representations of the Herbrand Universe" red pichler-mod : {'f['f['X1:A,'X2:A],'X3:A]} - ({'f['f['f['Y11:A,'Y12:A],'Y13:A],'Y13:A]} U {'f['f['Y31:A,'f['Y32:A,'Y33:A]],'Y34:A]} U {'f['f['Y41:A,'g['Y42:A]],'Y43:A]} U {'f['f['Y21:A,'Y21:A],'g['Y22:A]]}) eq {'f['f['f['A1:A,'A2:A],'a.A],'g['A3:A]]} U {'f['f['A1:A,'a.A],'f['A2:A,'A3:A]]} U {'f['f['g['A1:A],'a.A],'A2:A]} U {'f['f['a.A,'a.A],'a.A]} .