(def-constant t%true 
    "lambda(n:nn, truth)"
    (theory h-o-real-arithmetic))

(def-constant t%false 
    "lambda(n:nn, falsehood)"
    (theory h-o-real-arithmetic))

(def-constant t%not 
    "lambda(f:[nn,prop], lambda(n:nn, not(f(n))))"
    (theory h-o-real-arithmetic))

(def-constant t%and 
    "lambda(f,g:[nn,prop], lambda(n:nn, f(n) and g(n)))"
    (theory h-o-real-arithmetic))

(def-constant t%or 
    "lambda(f,g:[nn,prop], lambda(n:nn, f(n) or g(n)))"
    (theory h-o-real-arithmetic))

(def-constant t%nec 
    "lambda(f:[nn,prop], lambda(n:nn, forall(i:nn, n<=i implies f(i))))"
    (theory h-o-real-arithmetic))

(def-constant t%pos 
    "lambda(f:[nn,prop], lambda(n:nn, forsome(i:nn, n<=i implies f(i))))"
    (theory h-o-real-arithmetic))

(def-constant t%next 
    "lambda(f:[nn,prop], lambda(n:nn, f(n+1)))"
    (theory h-o-real-arithmetic))

(def-constant t%unless 
    "lambda(f,g:[nn,prop], 
          lambda(n:nn, 
              forall(i:nn, f(i) 
                  or 
              forsome(j:nn, n<=j and j<=i and g(i)))))"
    (theory h-o-real-arithmetic))

(def-constant t%prec 
    "lambda(f,g:[nn,prop], 
          lambda(n:nn, 
              forsome(i:nn, f(i) 
                  and 
              forall(j:nn, n<=j and j<=i implies not(g(i))))))"
    (theory h-o-real-arithmetic))

(def-theorem t%nec-t%true-rewrite 
    "t%nec(t%true) = t%true"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%nec-t%false-rewrite 
    "t%nec(t%false) = t%false"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%pos-t%true-rewrite 
    "t%pos(t%true) = t%true"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%pos-t%false-rewrite 
    "t%pos(t%false) = t%false"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%next-t%true-rewrite 
    "t%next(t%true) = t%true"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%next-t%false-rewrite 
    "t%next(t%false) = t%false"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%unless-t%true-p-rewrite 
    "forall(p:[zz,prop], t%unless(t%true,p) = t%true)"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%unless-p-t%true-rewrite 
    "forall(p:[zz,prop], t%unless(p,t%true) = t%true)"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%unless-t%false-p-rewrite 
    "forall(p:[zz,prop], t%unless(t%false,p) = p)"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%prec-t%true-p-rewrite 
    "forall(p:[zz,prop], t%prec(t%true,p) =$ t%not(p))"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%prec-p-t%true-rewrite 
    "forall(p:[zz,prop], t%prec(p,t%true) = t%false)"
    (theory h-o-real-arithmetic)
    (usages rewrite))

(def-theorem t%prec-t%false-p-rewrite 
    "forall(p:[zz,prop], t%prec(t%false,p) = t%false)"
    (theory h-o-real-arithmetic)
    (usages rewrite))