3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\documentclass[11pt,a4paper]{article}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\usepackage{german}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\usepackage{isolatin1}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\usepackage{amssymb}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\usepackage{epsfig}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\usepackage{moreverb}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\textwidth}{16cm}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\topmargin}{-1cm}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\evensidemargin}{0cm}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\oddsidemargin}{0cm}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\textheight}{24cm}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang% skip between paragraphs
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\parskip}{1ex}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang% ... and no indentation at start of a new paragraph
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\setlength{\parindent}{0ex}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\pagestyle{plain}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\thispagestyle{plain}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\begin{document}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\begin{verbatim}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangsorts Nat, Pos
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangsorts Pos < Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __! : Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __*__ : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __*__ : Pos * Pos -> Pos
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __+__ : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __+__ : Nat * Pos -> Pos
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __+__ : Pos * Nat -> Pos
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __-!__ : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __-?__ : Nat * Nat ->? Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __/?__ : Nat * Nat ->? Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __@@__ : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __^__ : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __div__ : Nat * Nat ->? Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop __mod__ : Nat * Nat ->? Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop max : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop min : Nat * Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop pre : Nat ->? Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop suc : Nat -> Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangop suc : Nat -> Pos
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred __<__ : Nat * Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred __<=__ : Nat * Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred __>__ : Nat * Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred __>=__ : Nat * Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred even : Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangpred odd : Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall X1:Nat . pre(suc(X1)) = X1 %(ga_selector_pre)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall X1:Nat; Y1:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . suc(X1) = suc(Y1) <=> X1 = Y1 %(ga_injective_suc)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall Y1:Nat . not 0 = suc(Y1) %(ga_disjoint_0_suc)%
e14bb000cb316e3cb100c3b6794eb61d4ccd6c9cHeng Jiangnot def pre(0) %(ga_selector_undef_pre_0) %
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jianggenerated{sort Nat; op 0 : Nat;
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang op suc : Nat -> Nat} %(ga_generated_Nat)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiang1 = suc(0) %(1_def_Nat)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiang2 = suc(1) %(2_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang3 = suc(2) %(3_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang4 = suc(3) %(4_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang5 = suc(4) %(5_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang6 = suc(5) %(6_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang7 = suc(6) %(7_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang8 = suc(7) %(8_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang9 = suc(8) %(9_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m:Nat; n:Nat . m @@ n = (m * suc(9)) + n %(decimal_def)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat; y:Nat . x + y = y + x %(ga_comm___+__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . x + (y + z) = (x + y) + z %(ga_assoc___+__)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat . x + 0 = x %(ga_right_unit___+__)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat . 0 + x = x %(ga_left_unit___+__)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat; y:Nat . x * y = y * x %(ga_comm___*__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . x * (y * z) = (x * y) * z %(ga_assoc___*__)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiangforall x:Nat . x * 1 = x %(ga_right_unit___*__)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiangforall x:Nat . 1 * x = x %(ga_left_unit___*__)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat; y:Nat . min(x, y) = min(y, x) %(ga_comm_min)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . min(x, min(y, z)) = min(min(x, y), z) %(ga_assoc_min)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat; y:Nat . max(x, y) = max(y, x) %(ga_comm_max)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . max(x, max(y, z)) = max(max(x, y), z) %(ga_assoc_max)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat . max(x, 0) = x %(ga_right_unit_max)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall x:Nat . max(0, x) = x %(ga_left_unit_max)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . 0 <= n %(leq_def1_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . not suc(n) <= 0 %(leq_def2_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . suc(m) <= suc(n) <=> m <= n %(leq_def3_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . m >= n <=> n <= m %(geq_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m < n <=> m <= n /\ not m = n %(less_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . m > n <=> n < m %(greater_def_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . even(0) %(even_0_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . even(suc(m)) <=> odd(m) %(even_suc_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . odd(m) <=> not even(m) %(odd_def_Nat)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiangforall m, n, r, s, t:Nat . 0 ! = 1 %(factorial_0)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . suc(n) ! = suc(n) * n ! %(factorial_suc)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . 0 + m = m %(add_0_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . suc(n) + m = suc(n + m) %(add_suc_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . 0 * m = 0 %(mult_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . suc(n) * m = (n * m) + m %(mult_suc_Nat)%
3c1951b861331e2833afe24888143c102be5ac85Heng Jiangforall m, n, r, s, t:Nat . m ^ 0 = 1 %(power_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m ^ suc(n) = m * (m ^ n) %(power_suc_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . min(m, n) = m when m <= n else n %(min_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . max(m, n) = n when m <= n else m %(max_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . n -! m = 0 if m > n %(subTotal_def1_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . n -! m = n -? m if m <= n %(subTotal_def2_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . def m -? n <=> m >= n %(sub_dom_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . m -? n = r <=> m = r + n %(sub_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . def m /? n <=> not n = 0 /\ m mod n = 0 %(divide_dom_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s, t:Nat . not def m /? 0 %(divide_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . (m /? n = r <=> m = r * n) if n > 0 %(divide_Pos_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . def m div n <=> not n = 0 %(div_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m div n = r <=>
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang exists s:Nat . m = (n * r) + s /\ s < n %(div_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . def m mod n <=> not n = 0 %(mod_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m mod n = s <=>
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang exists r:Nat . m = (n * r) + s /\ s < n %(mod_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . (r + s) * t = (r * t) + (s * t) %(distr1_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . t * (r + s) = (t * r) + (t * s) %(distr2_Nat)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall p:Nat . (p in Pos) <=> p > 0
3c1951b861331e2833afe24888143c102be5ac85Heng Jiang1 = suc(0) %(1_as_Pos_def)%
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiangforall m, n, r, s:Nat . min(m, 0) = 0 %(min_0)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m = ((m div n) * n) + (m mod n) if not n = 0 %(div_mod_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s:Nat
82c2daffbab78480bb7677bedf9899db82d7e7e4Heng Jiang . m ^ (r + s) = (m ^ r) * (m ^ s) %(power_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\end{verbatim}
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiang\section*{sorts $s < t$}
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiang\begin{verbatim}
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiangop f : s -> t
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiangop f : t -> t
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiangdef f((op d : s))
12d3759083c133ecb4922d925245326fc8e0ebe1Heng Jiang\end{verbatim}
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang\end{document}