lam.elf,32 term 5,58 lam 7,86 app 8,116 ord-red.elf,169 --> 4,84 beta1 7,153 lm1 9,193 apl1 12,274 apr1 15,349 -->* 20,448 id1 23,522 step1 25,544 <-> 31,624 refl 34,693 sym 36,713 trans39,752 red 43,813 par-red.elf,142 => 4,83 beta 7,169 ap 11,295 lm 15,391 =>* 20,508 id 23,599 ; 25,626 <=> 31,749 reduce 34,839 expand 37,881 ;; 40,922 par-lemmas.elf,100 identity 6,123 id_lam 8,162 id_app 11,277 append 17,419 append_id 19,479 append_step 20,510 par-cr.elf,364 subst 6,127 subst_idx 11,223 subst_beta 13,276 subst_ap 21,617 subst_lm 26,776 dia 35,1106 dia_bb 41,1311 dia_bal 50,1605 dia_alb 59,1906 dia_aa 68,2209 dia_ll 72,2345 strip 79,2580 strip_id 81,2649 strip_step 82,2681 conf 88,2859 conf_id 90,2930 conf_step 91,2964 cr 97,3142 cr_reduce 99,3195 cr_expand 100,3230 cr_compose 101,3265 ord-lemmas.elf,197 appd 6,121 appd_id 7,183 appd_step 8,211 lm1* 13,326 lm1*_id 17,408 lm1*_step 18,445 apl1* 21,540 apl1*_id 25,627 apl1*_step 26,655 apr1* 29,738 apr1*_id 33,825 apr1*_step 34,851 equiv.elf,476 eq1 6,109 eq1_beta 8,148 eq1_ap 18,451 eq1_lm 25,598 eq2 32,760 eq2_beta1 34,798 eq2_lm1 39,965 eq2_apl1 42,1068 eq2_apr1 46,1158 eq3 52,1277 eq3_id 54,1317 eq3_step 55,1338 eq4 61,1456 eq4_id 63,1496 eq4_step 64,1517 eq5 71,1651 eq5_red 73,1690 eq5_exp 75,1751 eq5_trans 77,1818 sym_pconv 83,1939 spc_red 85,1984 spc_exp 86,2031 spc_trans 87,2078 eq6 98,2385 eq6_refl 100,2424 eq6_sym 101,2458 eq6_trans 104,2541 eq6_red 107,2633 ord-cr.elf,27 cr_ord 4,82 cr_all 6,141 examples.quy,0