6 | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
9 ###### INTERPRETATION NUMBER 1 ######
10 ### (* disambiguation environment *)
11 alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
12 alias id mult = cic:/Coq/Init/Peano/mult.con
13 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
14 alias num (instance 0) = "natural number"
15 ### (* METASENV after disambiguation *)
17 ### (* TERM after disambiguation *)
20 fact / 0 : (nat->nat) :=
22 <[x:nat]nat>Cases x of
24 S => [x:nat](mult (S x) (fact x))
26 ](fact (S (S (S (S O)))))
27 ### (* TYPE_OF the disambiguated term *)
29 ### (* REDUCED disambiguated term *)
32 plus / 0 : (n:nat)(m:nat)nat :=
34 <[n0:nat]nat>Cases n of
36 S => [p:nat](S (plus p m))
40 plus / 0 : (n:nat)(m:nat)nat :=
42 <[n0:nat]nat>Cases n of
44 S => [p:nat](S (plus p m))
48 plus / 0 : (n:nat)(m:nat)nat :=
50 <[n0:nat]nat>Cases n of
52 S => [p:nat](S (plus p m))
56 plus / 0 : (n:nat)(m:nat)nat :=
58 <[n0:nat]nat>Cases n of
60 S => [p:nat](S (plus p m))
64 plus / 0 : (n:nat)(m:nat)nat :=
66 <[n0:nat]nat>Cases n of
68 S => [p:nat](S (plus p m))
72 plus / 0 : (n:nat)(m:nat)nat :=
74 <[n0:nat]nat>Cases n of
76 S => [p:nat](S (plus p m))
80 plus / 0 : (n:nat)(m:nat)nat :=
82 <[n0:nat]nat>Cases n of
84 S => [p:nat](S (plus p m))
88 plus / 0 : (n:nat)(m:nat)nat :=
90 <[n0:nat]nat>Cases n of
92 S => [p:nat](S (plus p m))
96 plus / 0 : (n:nat)(m:nat)nat :=
98 <[n0:nat]nat>Cases n of
100 S => [p:nat](S (plus p m))
104 plus / 0 : (n:nat)(m:nat)nat :=
106 <[n0:nat]nat>Cases n of
108 S => [p:nat](S (plus p m))
112 plus / 0 : (n:nat)(m:nat)nat :=
114 <[n0:nat]nat>Cases n of
116 S => [p:nat](S (plus p m))
120 plus / 0 : (n:nat)(m:nat)nat :=
122 <[n0:nat]nat>Cases n of
124 S => [p:nat](S (plus p m))
128 plus / 0 : (n:nat)(m:nat)nat :=
130 <[n0:nat]nat>Cases n of
132 S => [p:nat](S (plus p m))
136 plus / 0 : (n:nat)(m:nat)nat :=
138 <[n0:nat]nat>Cases n of
140 S => [p:nat](S (plus p m))
144 plus / 0 : (n:nat)(m:nat)nat :=
146 <[n0:nat]nat>Cases n of
148 S => [p:nat](S (plus p m))
152 plus / 0 : (n:nat)(m:nat)nat :=
154 <[n0:nat]nat>Cases n of
156 S => [p:nat](S (plus p m))
160 plus / 0 : (n:nat)(m:nat)nat :=
162 <[n0:nat]nat>Cases n of
164 S => [p:nat](S (plus p m))
168 plus / 0 : (n:nat)(m:nat)nat :=
170 <[n0:nat]nat>Cases n of
172 S => [p:nat](S (plus p m))
176 plus / 0 : (n:nat)(m:nat)nat :=
178 <[n0:nat]nat>Cases n of
180 S => [p:nat](S (plus p m))
184 plus / 0 : (n:nat)(m:nat)nat :=
186 <[n0:nat]nat>Cases n of
188 S => [p:nat](S (plus p m))
192 plus / 0 : (n:nat)(m:nat)nat :=
194 <[n0:nat]nat>Cases n of
196 S => [p:nat](S (plus p m))
200 plus / 0 : (n:nat)(m:nat)nat :=
202 <[n0:nat]nat>Cases n of
204 S => [p:nat](S (plus p m))
208 plus / 0 : (n:nat)(m:nat)nat :=
210 <[n0:nat]nat>Cases n of
212 S => [p:nat](S (plus p m))
216 plus / 0 : (n:nat)(m:nat)nat :=
218 <[n0:nat]nat>Cases n of
220 S => [p:nat](S (plus p m))
222 O O)) O)))))) O))))))))