This seems rather complicated! What about this: A => (B => C) = { X => Y == ¬X \/ Y } ¬A \/ (¬B \/ C) = {associativity} (¬A \/ ¬B) \/ C = { DeMorgan } ¬(A /\ B) \/ C = { X => Y == ¬X \/ Y } A /\ B => C E. Dave Tapley wrote:
Whoops, okay after two lines (thanks to oerjan) on #haskell I realise that yes, it is as easy as it should have been.
For completeness:
[A /\ B]1 ------------ (/\ E1) [A => (B => C)]2 A ------------------------------------------------- (=> E) B => C [A /\ B]1 ------------ (/\ E2) B B => C ------------------------------------------------- (=> E) C ------------------ (=> I)1 (A /\ B) => C
------------------------------------------------ (=> I)2 (A => (B => C)) => ((A /\ B) => C)
Learning is fun :)
Dave, _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe