TYPE Nat14 IS
  SORTS
    boolean, Nat14
  OPNS
    true, false: -> boolean
    n1, n2, n3, n4: -> Nat14
    succ, pred: Nat14 -> Nat14
    _ plus _: Nat14, Nat14 -> Nat14
    _ eq _: Nat14, Nat14 -> boolean
  EQNS
    OFSORT Nat14
    FORALL m, n: Nat14
      n2 = succ (n1) ;
      n3 = succ (succ (n1)) ;
      n4 = succ (n3) ;
      pred (m) = succ (succ (succ (m))) ;
      m plus succ (n) = succ (m plus n) ;
      m plus n1 = succ (m) ;
      succ (succ (succ (succ (n1)))) = n1 ;
      succ (succ (succ (succ (succ (m))))) = succ (m) ;

    OFSORT boolean
    FORALL x, y: Nat14
      x eq x = true ;
      x eq succ (x) = false ;
      x eq succ (succ (x)) = false ;
      x eq succ (succ (succ (x))) = false ;
      x eq succ (succ (succ (succ (x)))) = true ;
      n1 eq succ (succ (succ (succ (y)))) = n1 eq y ;
      succ (x) eq y = x eq succ (succ (succ (y))) ;
  ENDTYPE
