\documentclass[11pt,a4paper]{article}

\usepackage{german}

\usepackage{isolatin1}

\usepackage{amssymb}

\usepackage{epsfig}

\usepackage{moreverb}

\setlength{\textwidth}{16cm}

\setlength{\topmargin}{-1cm}

\setlength{\evensidemargin}{0cm}

\setlength{\oddsidemargin}{0cm}

\setlength{\textheight}{24cm}

% skip between paragraphs

\setlength{\parskip}{1ex}

% ... and no indentation at start of a new paragraph

\setlength{\parindent}{0ex}

\pagestyle{plain}

\thispagestyle{plain}

\begin{document}

\part*{Test}

\section*{Numbers.Nat}

\begin{verbatim}

sorts Nat, Pos

sorts Pos < Nat

op 0 : Nat

op 1 : Nat

op 1 : Pos

op 2 : Nat

op 3 : Nat

op 4 : Nat

op 5 : Nat

op 6 : Nat

op 7 : Nat

op 8 : Nat

op 9 : Nat

op __! : Nat -> Nat

op __*__ : Nat * Nat -> Nat

op __*__ : Pos * Pos -> Pos

op __+__ : Nat * Nat -> Nat

op __+__ : Nat * Pos -> Pos

op __+__ : Pos * Nat -> Pos

op __-!__ : Nat * Nat -> Nat

op __-?__ : Nat * Nat ->? Nat

op __/?__ : Nat * Nat ->? Nat

op __@@__ : Nat * Nat -> Nat

op __^__ : Nat * Nat -> Nat

op __div__ : Nat * Nat ->? Nat

op __mod__ : Nat * Nat ->? Nat

op max : Nat * Nat -> Nat

op min : Nat * Nat -> Nat

op pre : Nat ->? Nat

op suc : Nat -> Nat

op suc : Nat -> Pos

pred __<__ : Nat * Nat

pred __<=__ : Nat * Nat

pred __>__ : Nat * Nat

pred __>=__ : Nat * Nat

pred even : Nat

pred odd : Nat

forall X1:Nat . pre(suc(X1)) = X1 %(ga_selector_pre)%

forall X1:Nat; Y1:Nat

. suc(X1) = suc(Y1) <=> X1 = Y1 %(ga_injective_suc)%

forall Y1:Nat . not 0 = suc(Y1) %(ga_disjoint_0_suc)%

not def pre(0) %(ga_selector_undef_pre_0) %

generated{sort Nat; op 0 : Nat;

op suc : Nat -> Nat} %(ga_generated_Nat)%

1 = suc(0) %(1_def_Nat)%

2 = suc(1) %(2_def_Nat)%

3 = suc(2) %(3_def_Nat)%

4 = suc(3) %(4_def_Nat)%

5 = suc(4) %(5_def_Nat)%

6 = suc(5) %(6_def_Nat)%

7 = suc(6) %(7_def_Nat)%

8 = suc(7) %(8_def_Nat)%

9 = suc(8) %(9_def_Nat)%

forall m:Nat; n:Nat . m @@ n = (m * suc(9)) + n %(decimal_def)%

forall x:Nat; y:Nat . x + y = y + x %(ga_comm___+__)%

forall x:Nat; y:Nat; z:Nat

. x + (y + z) = (x + y) + z %(ga_assoc___+__)%

forall x:Nat . x + 0 = x %(ga_right_unit___+__)%

forall x:Nat . 0 + x = x %(ga_left_unit___+__)%

forall x:Nat; y:Nat . x * y = y * x %(ga_comm___*__)%

forall x:Nat; y:Nat; z:Nat

. x * (y * z) = (x * y) * z %(ga_assoc___*__)%

forall x:Nat . x * 1 = x %(ga_right_unit___*__)%

forall x:Nat . 1 * x = x %(ga_left_unit___*__)%

forall x:Nat; y:Nat . min(x, y) = min(y, x) %(ga_comm_min)%

forall x:Nat; y:Nat; z:Nat

. min(x, min(y, z)) = min(min(x, y), z) %(ga_assoc_min)%

forall x:Nat; y:Nat . max(x, y) = max(y, x) %(ga_comm_max)%

forall x:Nat; y:Nat; z:Nat

. max(x, max(y, z)) = max(max(x, y), z) %(ga_assoc_max)%

forall x:Nat . max(x, 0) = x %(ga_right_unit_max)%

forall x:Nat . max(0, x) = x %(ga_left_unit_max)%

forall m, n, r, s, t:Nat . 0 <= n %(leq_def1_Nat)%

forall m, n, r, s, t:Nat . not suc(n) <= 0 %(leq_def2_Nat)%

forall m, n, r, s, t:Nat

. suc(m) <= suc(n) <=> m <= n %(leq_def3_Nat)%

forall m, n, r, s, t:Nat . m >= n <=> n <= m %(geq_def_Nat)%

forall m, n, r, s, t:Nat

. m < n <=> m <= n /\ not m = n %(less_def_Nat)%

forall m, n, r, s, t:Nat . m > n <=> n < m %(greater_def_Nat)%

forall m, n, r, s, t:Nat . even(0) %(even_0_Nat)%

forall m, n, r, s, t:Nat . even(suc(m)) <=> odd(m) %(even_suc_Nat)%

forall m, n, r, s, t:Nat . odd(m) <=> not even(m) %(odd_def_Nat)%

forall m, n, r, s, t:Nat . 0 ! = 1 %(factorial_0)%

forall m, n, r, s, t:Nat

. suc(n) ! = suc(n) * n ! %(factorial_suc)%

forall m, n, r, s, t:Nat . 0 + m = m %(add_0_Nat)%

forall m, n, r, s, t:Nat . suc(n) + m = suc(n + m) %(add_suc_Nat)%

forall m, n, r, s, t:Nat . 0 * m = 0 %(mult_0_Nat)%

forall m, n, r, s, t:Nat

. suc(n) * m = (n * m) + m %(mult_suc_Nat)%

forall m, n, r, s, t:Nat . m ^ 0 = 1 %(power_0_Nat)%

forall m, n, r, s, t:Nat

. m ^ suc(n) = m * (m ^ n) %(power_suc_Nat)%

forall m, n, r, s, t:Nat

. min(m, n) = m when m <= n else n %(min_def_Nat)%

forall m, n, r, s, t:Nat

. max(m, n) = n when m <= n else m %(max_def_Nat)%

forall m, n, r, s, t:Nat

. n -! m = 0 if m > n %(subTotal_def1_Nat)%

forall m, n, r, s, t:Nat

. n -! m = n -? m if m <= n %(subTotal_def2_Nat)%

forall m, n, r, s, t:Nat . def m -? n <=> m >= n %(sub_dom_Nat)%

forall m, n, r, s, t:Nat . m -? n = r <=> m = r + n %(sub_def_Nat)%

forall m, n, r, s, t:Nat

. def m /? n <=> not n = 0 /\ m mod n = 0 %(divide_dom_Nat)%

forall m, n, r, s, t:Nat . not def m /? 0 %(divide_0_Nat)%

forall m, n, r, s, t:Nat

. (m /? n = r <=> m = r * n) if n > 0 %(divide_Pos_Nat)%

forall m, n, r, s, t:Nat

. def m div n <=> not n = 0 %(div_dom_Nat)%

forall m, n, r, s, t:Nat

. m div n = r <=>

exists s:Nat . m = (n * r) + s /\ s < n %(div_Nat)%

forall m, n, r, s, t:Nat

. def m mod n <=> not n = 0 %(mod_dom_Nat)%

forall m, n, r, s, t:Nat

. m mod n = s <=>

exists r:Nat . m = (n * r) + s /\ s < n %(mod_Nat)%

forall m, n, r, s, t:Nat

. (r + s) * t = (r * t) + (s * t) %(distr1_Nat)%

forall m, n, r, s, t:Nat

. t * (r + s) = (t * r) + (t * s) %(distr2_Nat)%

forall p:Nat . (p in Pos) <=> p > 0

1 = suc(0) %(1_as_Pos_def)%

forall m, n, r, s:Nat . min(m, 0) = 0 %(min_0)%

forall m, n, r, s:Nat

. m = ((m div n) * n) + (m mod n) if not n = 0 %(div_mod_Nat)%

forall m, n, r, s:Nat

. m ^ (r + s) = (m ^ r) * (m ^ s) %(power_Nat)%

\end{verbatim}

\section*{sorts $s < t$}

\begin{verbatim}

sorts s, t

sorts s < t

op c : s

op d : s

op d : t

op f : s -> t

op f : t -> t

def f(c)

def f((op d : s))

\end{verbatim}

\end{document}