Lines Matching refs:f2
33 | "B_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
34 in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
35 (*``^(ctl2mu_aux prop_type f1) /\ ^(ctl2mu_aux prop_type f2)`` *)
36 | "B_OR" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
37 in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
38 (*``^(ctl2mu_aux prop_type f1) \/ ^(ctl2mu_aux prop_type f2)`` *)
43 | "C_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
44 in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
45 | "C_OR" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
46 in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
49 | "C_EU" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
50 in mu_mu concRV (mu_disj (ctl2mu_aux f2 cons) (mu_conj (ctl2mu_aux f1 cons) (mu_dmd dotacn (mu_rv concRV)))) end
51 (*``mu "Q" .. ^(ctl2mu_aux prop_type f2) \/ (^(ctl2mu_aux prop_type f1) /\ (<<".">> (RV "Q")))``*)