Lines Matching refs:f2
801 (addFrmlToGraph g (U f1 f2) =
802 if MEM (U f1 f2) (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo))
804 else addNode <| frml := (U f1 f2); is_final := T
816 >- (Cases_on `?f1 f2. f = U f1 f2`
819 >> Cases_on `���y. U f1 f2 = (SND y).frml
823 >> qexists_tac `(g.next,<|frml := U f1 f2;
930 ==> (SORTED (��f1 f2. (FST f2).edge_grp <= (FST f1).edge_grp) fls
954 (��(f1:�� edgeLabelAA # num) (f2:�� edgeLabelAA # num).
955 (FST f2).edge_grp ��� (FST f1).edge_grp)`
1007 ==> ((?f1 f2. node.frml = U f1 f2) = node.is_final)`;
1757 f2:(�� edgeLabelAA # num).
1758 (FST f2).edge_grp ��� (FST f1).edge_grp)`