Zulip Chat Archive

Stream: new members

Topic: finish


view this post on Zulip Michael Beeson (Oct 03 2020 at 03:39):

An observation: ifinish cannot prove this:

h41: t  a  t  x  ¬t  x
h40: t  x  t  a
 t  a  t  x  t  a  ¬t  x

but if I manually do one 'split', then ifinish can do both the two new goals.


Last updated: May 14 2021 at 00:42 UTC