Prover is unable to prove a simple claim

[ehildenb]

The following definition fails to be proven (or take any steps) with the prover:

module ITEMS-SYNTAX
  imports DOMAINS-SYNTAX

  syntax Item ::= "A"
  syntax Items ::= List{Item, "|"}

endmodule

module ITEMS
  imports ITEMS-SYNTAX
  imports K-EQUAL
  imports INT

  configuration <k> $PGM:Items </k>

  rule <k> _ | IS => IS ... </k>

endmodule

module TEST-SPEC
  imports ITEMS

  claim <k> _:Items => .Items ... </k>
endmodule

To reproduce (K 5.1.156):

% kompile --version
K version:    5.1.165
Build date:   Fri Aug 27 00:41:16 UTC 2021

% kompile --backend haskell test.k --main-module ITEMS

% kprovex test.k --spec-module TEST-SPEC
kore-exec: [329391] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/dev/src/k/test.k:23:9-23:39
  #Not ( {
    _0
  #Equals
    .Items
  } )
#And
  <k>
    _0:Items ~> _DotVar1 ~> .
  </k>

Intuitively, what I expect to happen is this:

• The prover looks for rules that can apply to the LHS of the claim. The rule _ | IS => IS should be able to apply, which collects the path condition that #Exists I:Item . #Exists IS:Items . { _0:Items #Equals I | IS }, and then the prover can co-inductively apply the claim to the new state which discharges the proof.
• A second path is produced which has #Not (#Exists I:Item . #Exists IS:Items . { _0:Items #Equals I:Item | IS:Items }) (the remainder from applying the rule in step 1). I'm not sure if this step is possible, but then what the prover should do is show that this path condition means that _0:Items #Equals .Items (would require reasoning over all the available constructors). Then the prover can see that the proof immediately follows.

So I'm not sure if the second reasoning step (where we reason over available constructors to determine that _0:Items) is a desirable thing to add, but at the very least it seems that given the initial LHS, it should at least try the rule given in the semantics, which I cannot see that it's even attempting this rule.

Attached is the generated bug-report for this proof: test.tar.gz