Hi, it can be proven (by DECIDE_TAC) that,
|- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x but is there any conversion function available in HOL4 such that from LHS of above equation I can directly get the RHS - something like a canonical form? --Chun
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
