%BEGING S -> Main_ndList Main_leq Main_leq2 Main_ndList Main_ndNat Main_risers Main_risersAux Main_risersElse Main_risersThen F_5. F_5 x_40_leq x_40_leq2 x_40_ndList x_40_ndNat x_40_risers x_40_risersAux x_40_risersElse x_40_risersThen -> x_40_risers x_40_leq x_40_leq2 x_40_ndList x_40_ndNat x_40_risers x_40_risersAux x_40_risersElse x_40_risersThen End. Main_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> br (k Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (this_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen (F_4 k this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen)). F_4 k this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen -> this_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen (F_3 k x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen). F_3 k x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen -> k (Cons_leq x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_leq2 x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_ndList x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_ndNat x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_risers x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_risersAux x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_risersElse x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen) (Cons_risersThen x_34_leq x_34_leq2 x_34_ndList x_34_ndNat x_34_risers x_34_risersAux x_34_risersElse x_34_risersThen x_35_leq x_35_leq2 x_35_ndList x_35_ndNat x_35_risers x_35_risersAux x_35_risersElse x_35_risersThen). Main_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> br (k Z_leq Z_leq2 Z_ndList Z_ndNat Z_risers Z_risersAux Z_risersElse Z_risersThen) (this_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen (F_2 k)). F_2 k x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen -> k (S_leq x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_leq2 x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_ndList x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_ndNat x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_risers x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_risersAux x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_risersElse x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen) (S_risersThen x_38_leq x_38_leq2 x_38_ndList x_38_ndNat x_38_risers x_38_risersAux x_38_risersElse x_38_risersThen). Main_leq dummy_y_leq dummy_y_leq2 dummy_y_ndList dummy_y_ndNat dummy_y_risers dummy_y_risersAux dummy_y_risersElse dummy_y_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq_Main. Main_leq2 dummy_px_leq dummy_px_leq2 dummy_px_ndList dummy_px_ndNat dummy_px_risers dummy_px_risersAux dummy_px_risersElse dummy_px_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq2_Main. Main_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risers_Main. Main_risersAux dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersAux_Main. Main_risersElse dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersElse_Main. Main_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersThen_Main. Cons_risers hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> tl_risersAux hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen k. Cons_risersAux hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> x_leq hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen k. Cons_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> k (Cons_leq (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_leq2 (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_ndList (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_ndNat (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_risers (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_risersAux (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_risersElse (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen) (Cons_risersThen (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen) tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen). Cons_risersElse hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> k (Cons_leq (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_leq2 (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_ndList (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_ndNat (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_risers (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_risersAux (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_risersElse (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen) (Cons_risersThen (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen). Cons_leq hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen dummy_y_leq dummy_y_leq2 dummy_y_ndList dummy_y_ndNat dummy_y_risers dummy_y_risersAux dummy_y_risersElse dummy_y_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq_Cons. Cons_leq2 hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen dummy_px_leq dummy_px_leq2 dummy_px_ndList dummy_px_ndNat dummy_px_risers dummy_px_risersAux dummy_px_risersElse dummy_px_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq2_Cons. Cons_ndList hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_Cons. Cons_ndNat hd_leq hd_leq2 hd_ndList hd_ndNat hd_risers hd_risersAux hd_risersElse hd_risersThen tl_leq tl_leq2 tl_ndList tl_ndNat tl_risers tl_risersAux tl_risersElse tl_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_Cons. Nil_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> k Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen. Nil_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> fail. Nil_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> fail. Nil_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> k (Cons_leq (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen (Cons_leq x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_leq2 x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndList x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_ndNat x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risers x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersAux x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersElse x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) (Cons_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen) Nil_leq Nil_leq2 Nil_ndList Nil_ndNat Nil_risers Nil_risersAux Nil_risersElse Nil_risersThen). Nil_leq dummy_y_leq dummy_y_leq2 dummy_y_ndList dummy_y_ndNat dummy_y_risers dummy_y_risersAux dummy_y_risersElse dummy_y_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq_Nil. Nil_leq2 dummy_px_leq dummy_px_leq2 dummy_px_ndList dummy_px_ndNat dummy_px_risers dummy_px_risersAux dummy_px_risersElse dummy_px_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq2_Nil. Nil_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_Nil. Nil_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_Nil. List_leq dummy_y_leq dummy_y_leq2 dummy_y_ndList dummy_y_ndNat dummy_y_risers dummy_y_risersAux dummy_y_risersElse dummy_y_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq_List. List_leq2 dummy_px_leq dummy_px_leq2 dummy_px_ndList dummy_px_ndNat dummy_px_risers dummy_px_risersAux dummy_px_risersElse dummy_px_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq2_List. List_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_List. List_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_List. List_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risers_List. List_risersAux dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersAux_List. List_risersElse dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersElse_List. List_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersThen_List. S_leq p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> y_leq2 p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen k. S_leq2 p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> px_leq p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen k. S_ndList p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_S. S_ndNat p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_S. S_risers p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risers_S. S_risersAux p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersAux_S. S_risersElse p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersElse_S. S_risersThen p_leq p_leq2 p_ndList p_ndNat p_risers p_risersAux p_risersElse p_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersThen_S. Z_leq y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> Cons_risers y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen (Cons_leq y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_leq2 y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_ndList y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_ndNat y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risers y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersAux y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersElse y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersThen y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (F_1 k x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen). F_1 k x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen x_0_leq x_0_leq2 x_0_ndList x_0_ndNat x_0_risers x_0_risersAux x_0_risersElse x_0_risersThen -> x_0_risersThen x_leq x_leq2 x_ndList x_ndNat x_risers x_risersAux x_risersElse x_risersThen x_0_leq x_0_leq2 x_0_ndList x_0_ndNat x_0_risers x_0_risersAux x_0_risersElse x_0_risersThen k. Z_leq2 px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> Cons_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen (Cons_leq this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_leq2 this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersAux this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersElse this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (Cons_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen) (F_0 k px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen). F_0 k px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen x_5_leq x_5_leq2 x_5_ndList x_5_ndNat x_5_risers x_5_risersAux x_5_risersElse x_5_risersThen -> x_5_risersElse (S_leq px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_leq2 px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_ndList px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_ndNat px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_risers px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_risersAux px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_risersElse px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) (S_risersThen px_leq px_leq2 px_ndList px_ndNat px_risers px_risersAux px_risersElse px_risersThen) x_5_leq x_5_leq2 x_5_ndList x_5_ndNat x_5_risers x_5_risersAux x_5_risersElse x_5_risersThen k. Z_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_Z. Z_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_Z. Z_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risers_Z. Z_risersAux dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersAux_Z. Z_risersElse dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersElse_Z. Z_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersThen_Z. Nat_leq y_leq y_leq2 y_ndList y_ndNat y_risers y_risersAux y_risersElse y_risersThen etc_leq etc_leq2 etc_ndList etc_ndNat etc_risers etc_risersAux etc_risersElse etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> fail. Nat_leq2 dummy_px_leq dummy_px_leq2 dummy_px_ndList dummy_px_ndNat dummy_px_risers dummy_px_risersAux dummy_px_risersElse dummy_px_risersThen dummy_etc_leq dummy_etc_leq2 dummy_etc_ndList dummy_etc_ndNat dummy_etc_risers dummy_etc_risersAux dummy_etc_risersElse dummy_etc_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_leq2_Nat. Nat_ndList this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndList_Nat. Nat_ndNat this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_ndNat_Nat. Nat_risers this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risers_Nat. Nat_risersAux dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersAux_Nat. Nat_risersElse dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersElse_Nat. Nat_risersThen dummy_x_leq dummy_x_leq2 dummy_x_ndList dummy_x_ndNat dummy_x_risers dummy_x_risersAux dummy_x_risersElse dummy_x_risersThen this_leq this_leq2 this_ndList this_ndNat this_risers this_risersAux this_risersElse this_risersThen k -> method_undefined_risersThen_Nat. End x_42 x_43 x_44 x_45 x_46 x_47 x_48 x_49 -> end. %ENDG %BEGINA q0 end -> . q0 br -> q0 q0. %ENDA