(Bind b) \Rightarrow
match b with [
Abbr \Rightarrow
- (S (plus (weight_map A N map w) (weight_map A N (wadd map (S (weight_map A N map w))) u)))
+ (S ((weight_map A N map w) + (weight_map A N (wadd map (S (weight_map A N map w))) u)))
| Abst \Rightarrow
- (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+ (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
| Void \Rightarrow
- (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+ (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
]
| (Flat a) \Rightarrow
- (S (plus (weight_map A N map w) (weight_map A N map u)))
+ (S ((weight_map A N map w) + (weight_map A N map u)))
]
| (TGRef y n) \Rightarrow O
].
-definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)).
+definition weight: \forall A,N. T A N \to nat \def
+ \lambda A,N.
+ (weight_map A N (\lambda _.O)).
-definition tlt : \forall A,N. T A N \to T A N \to Prop \def \lambda A,N. \lambda t1,t2. (lt (weight A N t1) (weight A N t2)).
\ No newline at end of file
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def
+ \lambda A,N,t1,t2.
+ weight A N t1 < weight A N t2.