6 | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
9 ### (* METASENV after disambiguation *)
11 ### (* TERM after disambiguation *)
14 fact / 0 : (nat->nat) :=
16 <[x:nat]nat>Cases x of
18 S => [x:nat](mult (S x) (fact x))
20 ](fact (S (S (S (S O)))))
21 ### (* TYPE_OF the disambiguated term *)
23 ### (* REDUCED disambiguated term *)
26 plus / 0 : (n:nat)(nat->nat) :=
28 <[n0:nat]nat>Cases n of
30 S => [p:nat](S (plus p m))
34 plus / 0 : (n:nat)(nat->nat) :=
36 <[n0:nat]nat>Cases n of
38 S => [p:nat](S (plus p m))
42 plus / 0 : (n:nat)(nat->nat) :=
44 <[n0:nat]nat>Cases n of
46 S => [p:nat](S (plus p m))
50 plus / 0 : (n:nat)(nat->nat) :=
52 <[n0:nat]nat>Cases n of
54 S => [p:nat](S (plus p m))
58 plus / 0 : (n:nat)(nat->nat) :=
60 <[n0:nat]nat>Cases n of
62 S => [p:nat](S (plus p m))
66 plus / 0 : (n:nat)(nat->nat) :=
68 <[n0:nat]nat>Cases n of
70 S => [p:nat](S (plus p m))
74 plus / 0 : (n:nat)(nat->nat) :=
76 <[n0:nat]nat>Cases n of
78 S => [p:nat](S (plus p m))
82 plus / 0 : (n:nat)(nat->nat) :=
84 <[n0:nat]nat>Cases n of
86 S => [p:nat](S (plus p m))
90 plus / 0 : (n:nat)(nat->nat) :=
92 <[n0:nat]nat>Cases n of
94 S => [p:nat](S (plus p m))
98 plus / 0 : (n:nat)(nat->nat) :=
100 <[n0:nat]nat>Cases n of
102 S => [p:nat](S (plus p m))
106 plus / 0 : (n:nat)(nat->nat) :=
108 <[n0:nat]nat>Cases n of
110 S => [p:nat](S (plus p m))
114 plus / 0 : (n:nat)(nat->nat) :=
116 <[n0:nat]nat>Cases n of
118 S => [p:nat](S (plus p m))
122 plus / 0 : (n:nat)(nat->nat) :=
124 <[n0:nat]nat>Cases n of
126 S => [p:nat](S (plus p m))
130 plus / 0 : (n:nat)(nat->nat) :=
132 <[n0:nat]nat>Cases n of
134 S => [p:nat](S (plus p m))
138 plus / 0 : (n:nat)(nat->nat) :=
140 <[n0:nat]nat>Cases n of
142 S => [p:nat](S (plus p m))
146 plus / 0 : (n:nat)(nat->nat) :=
148 <[n0:nat]nat>Cases n of
150 S => [p:nat](S (plus p m))
154 plus / 0 : (n:nat)(nat->nat) :=
156 <[n0:nat]nat>Cases n of
158 S => [p:nat](S (plus p m))
162 plus / 0 : (n:nat)(nat->nat) :=
164 <[n0:nat]nat>Cases n of
166 S => [p:nat](S (plus p m))
170 plus / 0 : (n:nat)(nat->nat) :=
172 <[n0:nat]nat>Cases n of
174 S => [p:nat](S (plus p m))
178 plus / 0 : (n:nat)(nat->nat) :=
180 <[n0:nat]nat>Cases n of
182 S => [p:nat](S (plus p m))
186 plus / 0 : (n:nat)(nat->nat) :=
188 <[n0:nat]nat>Cases n of
190 S => [p:nat](S (plus p m))
194 plus / 0 : (n:nat)(nat->nat) :=
196 <[n0:nat]nat>Cases n of
198 S => [p:nat](S (plus p m))
202 plus / 0 : (n:nat)(nat->nat) :=
204 <[n0:nat]nat>Cases n of
206 S => [p:nat](S (plus p m))
210 plus / 0 : (n:nat)(nat->nat) :=
212 <[n0:nat]nat>Cases n of
214 S => [p:nat](S (plus p m))
216 O O)) O)))))) O))))))))