-interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun12 __ (or_f_minus_star _ _) r).
-interpretation "o-relation f⎻" 'OR_f_minus r = (fun12 __ (or_f_minus _ _) r).
-interpretation "o-relation f*" 'OR_f_star r = (fun12 __ (or_f_star _ _) r).
+interpretation "o-relation f⎻*" 'OR_f_minus_star r = (fun12 ?? (or_f_minus_star ? ?) r).
+interpretation "o-relation f⎻" 'OR_f_minus r = (fun12 ?? (or_f_minus ? ?) r).
+interpretation "o-relation f*" 'OR_f_star r = (fun12 ?? (or_f_star ? ?) r).