Lines Matching refs:a1
715 ������a1 i1 b1. p1 = pair a1 (pair i1 b1)���
718 qabbrev_tac ���N1 = LENGTH (pair a1 (pair i1 b1))��� >>
723 qabbrev_tac���ARG = pair (n2bl N1) (pair (n2bl SIb_i) (pair a1 (pair i1 b1) ++ pair i2 b2))��� >>
729 ���LENGTH (pair a1 (pair i1 b1)) ��� LENGTH (pair (n2bl y) (pair (n2bl (print_index ��� nblfst_i)) []))���
731 ���2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2)) + 10 ���
733 ���2 * ��� (2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2))) + 5 <= 2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2)) + 10 ��� 2 * ��� y + (2 * ��� (print_index ��� nblfst_i) + 2) + 10 <= 2 * ��� y + (3 * ��� (print_index ��� nblfst_i) + 23)��� suffices_by metis_tac[LESS_EQ_TRANS] >> rw[] >>
734 ���2 * ��� (2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2))) + 5 ���
735 2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2)) + 5 + 3��� suffices_by fs[] >>
736 qabbrev_tac���abi = 2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2))��� >> fs[] >>