module HomeworkSixteen

%default total

data Term = T | F | Q | And Term Term

data Val : Term -> Type where
  ValT : Val T
  ValF : Val F
  ValQ : Val Q

infixl 10 |->
data (|->) : Term -> Term -> Type where
  AndFirst : (t1 |-> t1') -> (And t1 t2) |-> (And t1' t2)
  AndSecond : Val t1 -> (t2 |-> t2') -> (And t1 t2) |-> (And t1 t2')
  AndF : Val t2 -> And F t2 |-> F
  AndT : Val t2 -> And T t2 |-> t2
  AndQF : And Q F |-> F
  AndQT : And Q T |-> Q
  AndQQ : And Q Q |-> Q

infixl 10 |-->
data (|-->) : Term -> Term -> Type where
  AndLFirst : (t1 |--> t1') -> (And t1 t2) |--> (And t1' t2)
  AndLSecond : Val t1 -> (t2 |--> t2') -> (And t1 t2) |--> (And t1 t2')
  AndLF : And F t2 |--> F
  AndLT : And T t2 |--> t2
  AndLQF : And Q F |--> F
  AndLQT : And Q T |--> Q
  AndLQQ : And Q Q |--> Q

infixl 10 !!
data (!!) : Term -> Term -> Type where
  SemT : T !! T
  SemF : F !! F
  SemQ : Q !! Q
  SemAndF : t1 !! F -> And t1 t2 !! F
  SemAndT : t1 !! T -> t2 !! v -> And t1 t2 !! v
  SemAndQF : t1 !! Q -> t2 !! F -> And t1 t2 !! F
  SemAndQ : t1 !! Q -> Either (t2 !! T) (t2 !! Q) -> And t1 t2 !! Q