An idris warm-up. Show this finite function forms a semi-lattice.

gistfile1.hs

data AndState = Bot | TrueBot | BotTrue | TrueTrue | F

total
myjoin : AndState -> AndState -> AndState
myjoin TrueBot BotTrue = TrueTrue
myjoin TrueTrue TrueBot = TrueTrue
myjoin TrueTrue BotTrue = TrueTrue
myjoin Bot x = x
myjoin F  _  = F
-- myjoin x y = myjoin y x
-- Manuallly writing all these out for the totality checker:
myjoin BotTrue TrueBot = TrueTrue
myjoin TrueBot TrueTrue  = TrueTrue
myjoin BotTrue TrueTrue  = TrueTrue
myjoin x Bot = x
myjoin _  F  = F
-- Manually writing out reflexive cases too:
myjoin TrueBot  TrueBot  = TrueBot
myjoin BotTrue  BotTrue  = BotTrue 
myjoin TrueTrue TrueTrue = TrueTrue

comm : (a:AndState) -> (b:AndState) -> (myjoin a b = myjoin b a)
comm Bot TrueBot = ?comm1
comm a b = ?comm2