reproving goals in TryWhy3
The attached file demonstrates a strange behaviour in TryWhy3. The "move" function cannot be proved at one go with the maximum amount of steps — okay. So we split it, and try to prove each subgoal separately — okay. The second "type invariant" subgoal cannot be prove with the maximum amount of steps — disappointing, but okay. HOWEVER, if now, after splitting, I select the parent node (full VC for "move") and try to reprove it with 1000 steps, every subgoal is proved — and this is not okay! Normally, this should produce exactly the same outcome when I try to reprove the subgoal.
Any ideas?