Antileft patterns remain for [owise] rules

[Baltoli]

Related to: #3035

@dwightguth identifies that rules with owise are still having priority predicates generated for them:

 axiom{R} \implies{R} (
    \and{R} (
      \not{R} (
        \or{R} (
          \exists{R} (Var'Unds'Gen0:SortBool{},
            \and{R} (
              \top{R}(),
              \and{R} (
                \in{SortK{}, R} (
                  X0:SortK{},
                  kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen0:SortBool{}),dotk{}())
                ),
                \top{R} ()
              )
          )),
          \bottom{R}()
        )
      ),
      \and{R}(
        \top{R}(),
        \and{R} (
          \in{SortK{}, R} (
            X0:SortK{},
            VarK:SortK{}
          ),
          \top{R} ()
        )
    )),
    \equals{SortBool{},R} (
      LblisBool{}(X0:SortK{}),
     \and{SortBool{}} (
       \dv{SortBool{}}("false"),
        \top{SortBool{}}())))

[dwightguth]

I believe it's possible that the antileft patterns for rewrite rules were removed but not the ones for equations.

[Baltoli]

I want to confirm that removing this kind of antileft is what we intended with the original proposal in #3035; as I recall it that change was specifically to do with priority predicate antilefts.

What is the actual KORE that you'd expect to see here for this rule @dwightguth? I can't find a version with the \not removed that is currently accepted by the LLVM backend, which makes me suspicious.

[Baltoli]

If the KORE you'd expect to see isn't accepted by the backend, we'll need to do another multi-stage change. It is also possible I just haven't found the right form yet, though

[ana-pantilie]

Let's not remove antileft patterns for equations just yet, the old backend still depends on these for some reason which has been very hard to investigate runtimeverification/haskell-backend#2250

[dwightguth]

sigh I wish I'd known that was the plan. I've waited a couple weeks to continue progress on something because I thought it would be easier to implement once we finished this change, but that's not really true if we're only removing the patterns from top level rules. It would have saved a lot of time if I'd known I wasn't actually blocked on this change. Oh well...