orass Show Code edit
## Associative Property of OR
## right('Associate', 'R') left('Associate', 'L')
thm (orass () () (<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch)))
(\/ ph ps) ch orcom
(<-> (\/ (\/ ph ps) ch) (\/ ch (\/ ph ps)))
ch ph ps or12
(<-> (\/ ch (\/ ph ps)) (\/ ph (\/ ch ps)))
bitri
(<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ch ps)))
ch ps orcom
(<-> (\/ ch ps) (\/ ps ch))
ph orbi2i
(<-> (\/ ph (\/ ch ps)) (\/ ph (\/ ps ch)))
bitri
(<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch)))
)
edit