1090 kk_subset r1 r2 |
1090 kk_subset r1 r2 |
1091 end |
1091 end |
1092 else |
1092 else |
1093 kk_rel_eq r1 r2 |
1093 kk_rel_eq r1 r2 |
1094 end) |
1094 end) |
|
1095 | Op2 (The, T, _, u1, u2) => |
|
1096 to_f_with_polarity polar |
|
1097 (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2)) |
|
1098 | Op2 (Eps, T, _, u1, u2) => |
|
1099 to_f_with_polarity polar |
|
1100 (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) |
1095 | Op2 (Apply, T, _, u1, u2) => |
1101 | Op2 (Apply, T, _, u1, u2) => |
1096 (case (polar, rep_of u1) of |
1102 (case (polar, rep_of u1) of |
1097 (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1) |
1103 (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1) |
1098 | _ => |
1104 | _ => |
1099 to_f_with_polarity polar |
1105 to_f_with_polarity polar |