simplifySenTest.tex revision 12d3759083c133ecb4922d925245326fc8e0ebe1
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
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall X1:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . pre((op suc : Nat -> Nat)(X1 : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang X1 : Nat %(ga_selector_pre)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall X1:Nat; Y1:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op suc : Nat -> Nat)(X1 : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op suc : Nat -> Nat)(Y1 : Nat) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang X1 : Nat = Y1 : Nat %(ga_injective_suc)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall Y1:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . not 0 = (op suc : Nat -> Nat)(Y1 : Nat) %(ga_disjoint_0_suc)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng 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)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang(op 1 : Nat) = (op suc : Nat -> Nat)(0) %(1_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang2 = (op suc : Nat -> Nat)((op 1 : Nat)) %(2_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang3 = (op suc : Nat -> Nat)(2) %(3_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang4 = (op suc : Nat -> Nat)(3) %(4_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang5 = (op suc : Nat -> Nat)(4) %(5_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang6 = (op suc : Nat -> Nat)(5) %(6_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang7 = (op suc : Nat -> Nat)(6) %(7_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang8 = (op suc : Nat -> Nat)(7) %(8_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang9 = (op suc : Nat -> Nat)(8) %(9_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m:Nat; n:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat @@ n : Nat =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(m : Nat, (op suc : Nat -> Nat)(9)),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang n : Nat) %(decimal_def)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)(x : Nat, y : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)(y : Nat, x : Nat) %(ga_comm___+__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)(x : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)(y : Nat, z : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __+__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(x : Nat, y : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang z : Nat) %(ga_assoc___+__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)(x : Nat, 0) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang x : Nat %(ga_right_unit___+__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)(0, x : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang x : Nat %(ga_left_unit___+__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)(x : Nat, y : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(y : Nat, x : Nat) %(ga_comm___*__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)(x : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(y : Nat, z : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(x : Nat, y : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang z : Nat) %(ga_assoc___*__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)(x : Nat, (op 1 : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang x : Nat %(ga_right_unit___*__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)((op 1 : Nat), x : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang x : Nat %(ga_left_unit___*__)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . min(x : Nat, y : Nat) = min(y : Nat, x : Nat) %(ga_comm_min)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . min(x : Nat, min(y : Nat, z : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang min(min(x : Nat, y : Nat), z : Nat) %(ga_assoc_min)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . max(x : Nat, y : Nat) = max(y : Nat, x : Nat) %(ga_comm_max)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat; y:Nat; z:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . max(x : Nat, max(y : Nat, z : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang max(max(x : Nat, y : Nat), z : Nat) %(ga_assoc_max)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat . max(x : Nat, 0) = x : Nat %(ga_right_unit_max)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall x:Nat . max(0, x : Nat) = x : Nat %(ga_left_unit_max)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred __<=__ : Nat * Nat)(0, n : Nat) %(leq_def1_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . not (pred __<=__ : Nat * Nat)((op suc : Nat -> Nat)(n : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang 0) %(leq_def2_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred __<=__ : Nat * Nat)((op suc : Nat -> Nat)(m : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op suc : Nat -> Nat)(n : Nat)) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __<=__ : Nat * Nat)(m : Nat, n : Nat) %(leq_def3_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred __>=__ : Nat * Nat)(m : Nat, n : Nat) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __<=__ : Nat * Nat)(n : Nat, m : Nat) %(geq_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred __<__ : Nat * Nat)(m : Nat, n : Nat) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __<=__ : Nat * Nat)(m : Nat, n : Nat)
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang /\ not m : Nat = n : Nat %(less_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred __>__ : Nat * Nat)(m : Nat, n : Nat) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __<__ : Nat * Nat)(n : Nat, m : Nat) %(greater_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat . (pred even : Nat)(0) %(even_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred even : Nat)((op suc : Nat -> Nat)(m : Nat)) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred odd : Nat)(m : Nat) %(even_suc_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (pred odd : Nat)(m : Nat) <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang not (pred even : Nat)(m : Nat) %(odd_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat . 0 ! = (op 1 : Nat) %(factorial_0)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op suc : Nat -> Nat)(n : Nat) ! =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)((op suc : Nat -> Nat)(n : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang n : Nat !) %(factorial_suc)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)(0, m : Nat) = m : Nat %(add_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __+__ : Nat * Nat -> Nat)((op suc : Nat -> Nat)(n : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op suc : Nat -> Nat)((op __+__ : Nat * Nat -> Nat)(n : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat)) %(add_suc_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)(0, m : Nat) = 0 %(mult_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)((op suc : Nat -> Nat)(n : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(n : Nat, m : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat) %(mult_suc_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat ^ 0 = (op 1 : Nat) %(power_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat ^ (op suc : Nat -> Nat)(n : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(m : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat ^ n : Nat) %(power_suc_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . min(m : Nat, n : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat when m : Nat <= n : Nat else n : Nat %(min_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . max(m : Nat, n : Nat) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang n : Nat when m : Nat <= n : Nat else m : Nat %(max_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . n : Nat -! m : Nat = 0 if
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __>__ : Nat * Nat)(m : Nat, n : Nat) %(subTotal_def1_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . n : Nat -! m : Nat = n : Nat -? m : Nat if
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __<=__ : Nat * Nat)(m : Nat, n : Nat) %(subTotal_def2_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . def m : Nat -? n : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __>=__ : Nat * Nat)(m : Nat, n : Nat) %(sub_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat -? n : Nat = r : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)(r : Nat, n : Nat) %(sub_def_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . def m : Nat /? n : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang not n : Nat = 0 /\ m : Nat mod n : Nat = 0 %(divide_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat . not def m : Nat /? 0 %(divide_0_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (m : Nat /? n : Nat = r : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat = (op __*__ : Nat * Nat -> Nat)(r : Nat, n : Nat)) if
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (pred __>__ : Nat * Nat)(n : Nat, 0) %(divide_Pos_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . def m : Nat div n : Nat <=> not n : Nat = 0 %(div_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat div n : Nat = r : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang exists s:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(n : Nat, r : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang /\ (pred __<__ : Nat * Nat)(s : Nat, n : Nat) %(div_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . def m : Nat mod n : Nat <=> not n : Nat = 0 %(mod_dom_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat mod n : Nat = s : Nat <=>
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang exists r:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(n : Nat, r : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang /\ (pred __<__ : Nat * Nat)(s : Nat, n : Nat) %(mod_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)((op __+__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(r : Nat, s : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(r : Nat, t : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(s : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang t : Nat)) %(distr1_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s, t:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (op __*__ : Nat * Nat -> Nat)(t : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)(r : Nat, s : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat *
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang Nat -> Nat)(t : Nat, r : Nat),
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(t : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang s : Nat)) %(distr2_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . (p : Nat in Pos) <=> (pred __>__ : Nat * Nat)(p : Nat, 0)
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang(op 1 : Nat) = (op suc : Nat -> Nat)(0) %(1_as_Pos_def)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s:Nat . min(m : Nat, 0) = 0 %(min_0)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __+__ : Nat * Nat -> Nat)((op __*__ : Nat * Nat -> Nat)(m : Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang div n : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat mod n : Nat) if
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang not n : Nat = 0 %(div_mod_Nat)%
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiangforall m, n, r, s:Nat
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang . m : Nat ^ ((op __+__ : Nat * Nat -> Nat)(r : Nat, s : Nat)) =
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang (op __*__ : Nat * Nat -> Nat)(m : Nat ^ r : Nat,
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang m : Nat ^ s : Nat)
3b53a2a53ce476a23adff0f911e0de231b101233Heng Jiang %(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}