Terme:
Imports:
union

Parameters:

Body:
sorts
  s1;
  s1 < s2
ops
  o : s1;
  p : s1->?s2;
  q : s1*s2->s2;
  schwachsinn : ?s2
preds
  p1 : s1;
  p2 : s1*s2;
  p3 : s1;
  p4 : s1*s2;
  p_null : ()

Axioms: