Lines Matching refs:f2
13 ��� (tempDNF_concr (DISJ f1 f2) = (tempDNF_concr f1) ++ (tempDNF_concr f2))
14 ��� (tempDNF_concr (CONJ f1 f2) =
16 let tDNF2 = tempDNF_concr f2 in
19 ��� (tempDNF_concr (U f1 f2) = [[U f1 f2]])
20 ��� (tempDNF_concr (R f1 f2) = [[R f1 f2]])`;
123 ��� (props_concr (DISJ f1 f2) = props_concr f1 ++ props_concr f2)
124 ��� (props_concr (CONJ f1 f2) = props_concr f1 ++ props_concr f2)
126 ��� (props_concr (U f1 f2) = props_concr f1 ++ props_concr f2)
127 ��� (props_concr (R f1 f2) = props_concr f1 ++ props_concr f2)`;
149 ��� (trans_concr (CONJ f1 f2) =
150 d_conj_concr (trans_concr f1) (trans_concr f2))
151 ��� (trans_concr (DISJ f1 f2) =
152 (trans_concr f1) ++ (trans_concr f2))
155 ��� (trans_concr (U f1 f2) =
156 (trans_concr f2) ++
158 [<| pos := [] ; neg := [] ; sucs := [U f1 f2] |>]))
159 ��� (trans_concr (R f1 f2) =
160 d_conj_concr (trans_concr f2)
161 (<| pos := [] ; neg := [] ; sucs := [R f1 f2] |> ::
763 (mlt1 (\f1 f2. f1 ��� tempSubForms f2 ��� ~(f1 = f2)))
2352 >- (`?f1 f2. x'.frml = U f1 f2` by metis_tac[until_iff_final_def]
2353 >> qexists_tac `f1` >> qexists_tac `f2` >> simp[]
2371 >> `U f1 f2 ��� concr2Abstr_states g` by metis_tac[IN_INTER]
2372 >> `MEM (U f1 f2) (graphStates g)`