purple is "running process on the command"
If that command is a by (simp add:lemma), then it went to infinite loop? Other than that, it led to No Subgoals! Is this a valid proof or not?
If it is just purple indefinitely, it means that it has not terminated yet. As I explained in the other thread, that means that the proof is not yet completed. The ‘No subgoals!’ you see is provisional in the sense that it assumes that the proof is valid (which it isn't if the
simp never terminates).
(@Manuel Eberl : I got confused when reading your sentence, but I guess "yeat complicated" -> yet completed)
Not sure what happened there. Probably general brain fault. :smile:
Thanks. At last I have found the necessary lemmas so now it works without problem.
Also, it used lots of processor and memory, that's why I thought of an infinite loop.
Last updated: Aug 13 2022 at 06:26 UTC