helm/gTopLevel/tests/fix00.cic.test

   1 let rec fact =
   2   \lambda x:nat.
   3     [\lambda x:nat. nat]
   4     match x:nat with
   5     [ O \Rightarrow 1
   6     | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
   7 in
   8 (fact 4)
   9 ### (* METASENV after disambiguation  *)
  10
  11 ### (* TERM after disambiguation      *)
  12 [fact:=
  13 Fix fact {
  14 fact / 0 : (nat->nat) :=
  15 [x:nat]
  16 <[x:nat]nat>Cases x of
  17  O => (S O)
  18  S => [x:nat](mult (S x) (fact x))
  19 end}
  20 ](fact (S (S (S (S O)))))
  21 ### (* TYPE_OF the disambiguated term *)
  22 nat
  23 ### (* REDUCED disambiguated term     *)
  24 (S (
  25 Fix plus {
  26 plus / 0 : (n:nat)(nat->nat) :=
  27 [n:nat][m:nat]
  28 <[n0:nat]nat>Cases n of
  29  O => m
  30  S => [p:nat](S (plus p m))
  31 end}
  32  (S (
  33 Fix plus {
  34 plus / 0 : (n:nat)(nat->nat) :=
  35 [n:nat][m:nat]
  36 <[n0:nat]nat>Cases n of
  37  O => m
  38  S => [p:nat](S (plus p m))
  39 end}
  40  O (S (
  41 Fix plus {
  42 plus / 0 : (n:nat)(nat->nat) :=
  43 [n:nat][m:nat]
  44 <[n0:nat]nat>Cases n of
  45  O => m
  46  S => [p:nat](S (plus p m))
  47 end}
  48  (S (
  49 Fix plus {
  50 plus / 0 : (n:nat)(nat->nat) :=
  51 [n:nat][m:nat]
  52 <[n0:nat]nat>Cases n of
  53  O => m
  54  S => [p:nat](S (plus p m))
  55 end}
  56  O O)) (S (
  57 Fix plus {
  58 plus / 0 : (n:nat)(nat->nat) :=
  59 [n:nat][m:nat]
  60 <[n0:nat]nat>Cases n of
  61  O => m
  62  S => [p:nat](S (plus p m))
  63 end}
  64  (S (
  65 Fix plus {
  66 plus / 0 : (n:nat)(nat->nat) :=
  67 [n:nat][m:nat]
  68 <[n0:nat]nat>Cases n of
  69  O => m
  70  S => [p:nat](S (plus p m))
  71 end}
  72  O O)) O)))))) (S (
  73 Fix plus {
  74 plus / 0 : (n:nat)(nat->nat) :=
  75 [n:nat][m:nat]
  76 <[n0:nat]nat>Cases n of
  77  O => m
  78  S => [p:nat](S (plus p m))
  79 end}
  80  (S (
  81 Fix plus {
  82 plus / 0 : (n:nat)(nat->nat) :=
  83 [n:nat][m:nat]
  84 <[n0:nat]nat>Cases n of
  85  O => m
  86  S => [p:nat](S (plus p m))
  87 end}
  88  O (S (
  89 Fix plus {
  90 plus / 0 : (n:nat)(nat->nat) :=
  91 [n:nat][m:nat]
  92 <[n0:nat]nat>Cases n of
  93  O => m
  94  S => [p:nat](S (plus p m))
  95 end}
  96  (S (
  97 Fix plus {
  98 plus / 0 : (n:nat)(nat->nat) :=
  99 [n:nat][m:nat]
 100 <[n0:nat]nat>Cases n of
 101  O => m
 102  S => [p:nat](S (plus p m))
 103 end}
 104  O O)) (S (
 105 Fix plus {
 106 plus / 0 : (n:nat)(nat->nat) :=
 107 [n:nat][m:nat]
 108 <[n0:nat]nat>Cases n of
 109  O => m
 110  S => [p:nat](S (plus p m))
 111 end}
 112  (S (
 113 Fix plus {
 114 plus / 0 : (n:nat)(nat->nat) :=
 115 [n:nat][m:nat]
 116 <[n0:nat]nat>Cases n of
 117  O => m
 118  S => [p:nat](S (plus p m))
 119 end}
 120  O O)) O)))))) (S (
 121 Fix plus {
 122 plus / 0 : (n:nat)(nat->nat) :=
 123 [n:nat][m:nat]
 124 <[n0:nat]nat>Cases n of
 125  O => m
 126  S => [p:nat](S (plus p m))
 127 end}
 128  (S (
 129 Fix plus {
 130 plus / 0 : (n:nat)(nat->nat) :=
 131 [n:nat][m:nat]
 132 <[n0:nat]nat>Cases n of
 133  O => m
 134  S => [p:nat](S (plus p m))
 135 end}
 136  O (S (
 137 Fix plus {
 138 plus / 0 : (n:nat)(nat->nat) :=
 139 [n:nat][m:nat]
 140 <[n0:nat]nat>Cases n of
 141  O => m
 142  S => [p:nat](S (plus p m))
 143 end}
 144  (S (
 145 Fix plus {
 146 plus / 0 : (n:nat)(nat->nat) :=
 147 [n:nat][m:nat]
 148 <[n0:nat]nat>Cases n of
 149  O => m
 150  S => [p:nat](S (plus p m))
 151 end}
 152  O O)) (S (
 153 Fix plus {
 154 plus / 0 : (n:nat)(nat->nat) :=
 155 [n:nat][m:nat]
 156 <[n0:nat]nat>Cases n of
 157  O => m
 158  S => [p:nat](S (plus p m))
 159 end}
 160  (S (
 161 Fix plus {
 162 plus / 0 : (n:nat)(nat->nat) :=
 163 [n:nat][m:nat]
 164 <[n0:nat]nat>Cases n of
 165  O => m
 166  S => [p:nat](S (plus p m))
 167 end}
 168  O O)) O)))))) (S (
 169 Fix plus {
 170 plus / 0 : (n:nat)(nat->nat) :=
 171 [n:nat][m:nat]
 172 <[n0:nat]nat>Cases n of
 173  O => m
 174  S => [p:nat](S (plus p m))
 175 end}
 176  (S (
 177 Fix plus {
 178 plus / 0 : (n:nat)(nat->nat) :=
 179 [n:nat][m:nat]
 180 <[n0:nat]nat>Cases n of
 181  O => m
 182  S => [p:nat](S (plus p m))
 183 end}
 184  O (S (
 185 Fix plus {
 186 plus / 0 : (n:nat)(nat->nat) :=
 187 [n:nat][m:nat]
 188 <[n0:nat]nat>Cases n of
 189  O => m
 190  S => [p:nat](S (plus p m))
 191 end}
 192  (S (
 193 Fix plus {
 194 plus / 0 : (n:nat)(nat->nat) :=
 195 [n:nat][m:nat]
 196 <[n0:nat]nat>Cases n of
 197  O => m
 198  S => [p:nat](S (plus p m))
 199 end}
 200  O O)) (S (
 201 Fix plus {
 202 plus / 0 : (n:nat)(nat->nat) :=
 203 [n:nat][m:nat]
 204 <[n0:nat]nat>Cases n of
 205  O => m
 206  S => [p:nat](S (plus p m))
 207 end}
 208  (S (
 209 Fix plus {
 210 plus / 0 : (n:nat)(nat->nat) :=
 211 [n:nat][m:nat]
 212 <[n0:nat]nat>Cases n of
 213  O => m
 214  S => [p:nat](S (plus p m))
 215 end}
 216  O O)) O)))))) O))))))))