```
(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))
```