- \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(eq_ind nat
-(S (plus (cweight c) (plus (tweight u) (tweight t)))) (\lambda (n: nat).(lt
-(plus (plus (cweight c) (tweight u)) (tweight t)) n)) (eq_ind_r nat (plus
-(plus (cweight c) (tweight u)) (tweight t)) (\lambda (n: nat).(lt (plus (plus
-(cweight c) (tweight u)) (tweight t)) (S n))) (le_n (S (plus (plus (cweight
-c) (tweight u)) (tweight t)))) (plus (cweight c) (plus (tweight u) (tweight
-t))) (plus_assoc_l (cweight c) (tweight u) (tweight t))) (plus (cweight c) (S
-(plus (tweight u) (tweight t)))) (plus_n_Sm (cweight c) (plus (tweight u)
-(tweight t))))))).
-(* COMMENTS
-Initial nodes: 179
-END *)
+ \lambda (_: K).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(let TMP_1
+\def (cweight c) in (let TMP_2 \def (tweight u) in (let TMP_3 \def (tweight
+t) in (let TMP_4 \def (plus TMP_2 TMP_3) in (let TMP_5 \def (plus TMP_1
+TMP_4) in (let TMP_6 \def (S TMP_5) in (let TMP_12 \def (\lambda (n:
+nat).(let TMP_7 \def (cweight c) in (let TMP_8 \def (tweight u) in (let TMP_9
+\def (plus TMP_7 TMP_8) in (let TMP_10 \def (tweight t) in (let TMP_11 \def
+(plus TMP_9 TMP_10) in (lt TMP_11 n))))))) in (let TMP_13 \def (cweight c) in
+(let TMP_14 \def (tweight u) in (let TMP_15 \def (plus TMP_13 TMP_14) in (let
+TMP_16 \def (tweight t) in (let TMP_17 \def (plus TMP_15 TMP_16) in (let
+TMP_24 \def (\lambda (n: nat).(let TMP_18 \def (cweight c) in (let TMP_19
+\def (tweight u) in (let TMP_20 \def (plus TMP_18 TMP_19) in (let TMP_21 \def
+(tweight t) in (let TMP_22 \def (plus TMP_20 TMP_21) in (let TMP_23 \def (S
+n) in (lt TMP_22 TMP_23)))))))) in (let TMP_25 \def (cweight c) in (let
+TMP_26 \def (tweight u) in (let TMP_27 \def (plus TMP_25 TMP_26) in (let
+TMP_28 \def (tweight t) in (let TMP_29 \def (plus TMP_27 TMP_28) in (let
+TMP_30 \def (S TMP_29) in (let TMP_31 \def (le_n TMP_30) in (let TMP_32 \def
+(cweight c) in (let TMP_33 \def (tweight u) in (let TMP_34 \def (tweight t)
+in (let TMP_35 \def (plus TMP_33 TMP_34) in (let TMP_36 \def (plus TMP_32
+TMP_35) in (let TMP_37 \def (cweight c) in (let TMP_38 \def (tweight u) in
+(let TMP_39 \def (tweight t) in (let TMP_40 \def (plus_assoc_l TMP_37 TMP_38
+TMP_39) in (let TMP_41 \def (eq_ind_r nat TMP_17 TMP_24 TMP_31 TMP_36 TMP_40)
+in (let TMP_42 \def (cweight c) in (let TMP_43 \def (tweight u) in (let
+TMP_44 \def (tweight t) in (let TMP_45 \def (plus TMP_43 TMP_44) in (let
+TMP_46 \def (S TMP_45) in (let TMP_47 \def (plus TMP_42 TMP_46) in (let
+TMP_48 \def (cweight c) in (let TMP_49 \def (tweight u) in (let TMP_50 \def
+(tweight t) in (let TMP_51 \def (plus TMP_49 TMP_50) in (let TMP_52 \def
+(plus_n_Sm TMP_48 TMP_51) in (eq_ind nat TMP_6 TMP_12 TMP_41 TMP_47
+TMP_52))))))))))))))))))))))))))))))))))))))))))))).