(weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1)) (le_plus_plus
(weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) (weight_map g t1) (H1
f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t z H))))).
(weight_map f0 t2)) (plus (weight_map g u1) (weight_map g t1)) (le_plus_plus
(weight_map f0 u2) (weight_map g u1) (weight_map f0 t2) (weight_map g t1) (H1
f0 g H4 H5) (H3 f0 g H4 H5)))))))))))) k)))))))) d u t z H))))).