More examples of llprover

Last modified: Fri Apr 30 06:59:13 2004 JST

a*b --> b*a
(a*b)*c <--> a*(b*c)
1*a <--> a
a+b --> b+a
(a+b)+c <--> a+(b+c)
0+a <--> a
a/\b --> b/\a
(a/\b)/\c <--> a/\(b/\c)
a/\a <--> a
top/\a <--> a
bot/\a <--> bot
a\/b --> b\/a
(a\/b)\/c <--> a\/(b\/c)
a\/a <--> a
bot\/a <--> a
top\/a <--> top
a/\(a\/b) <--> a
a\/(a/\b) <--> a
a, a->b --> b
a->(b->c) <--> (a*b)->c
!(a*c -> b), !(b*d*d -> c*d), a, c, d, d --> c*d (in ILLe)