+inductive alpha_uni : Type[0] ≝
+| bit : bool → alpha_uni
+| mark : bool → alpha_uni
+| grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
+
+inductive Qmatch : Type[0] ≝
+| qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
+| qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch
+| qm8 : Qmatch | qm9 : Qmatch
+| qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
+
+definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
+
+definition tmatch ≝ λs,c.
+match s with
+[ qm0 ⇒ match c with
+ [ grid ⇒ 〈qm1,〈grid,R〉〉
+ | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm1 ⇒ match c with
+ [ mark x ⇒ 〈qm2 x,〈bit x,R〉〉
+ | _ ⇒ 〈qm1,〈c,L〉〉 ]
+| qm2 x ⇒ match c with
+ [ bit y ⇒ 〈qm3 x,〈mark y,R〉〉
+ | grid ⇒ 〈qm3 x,〈grid,R〉〉
+ | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm3 x ⇒ match c with
+ [ mark y ⇒ match bool_eqb x y with
+ [ true ⇒ 〈qm4,〈bit y,R〉〉
+ | false ⇒ 〈qm5,〈bit y,R〉〉 ]
+ | _ ⇒ 〈qm3 x,〈c,R〉〉 ]
+| qm4 ⇒ match c with
+ [ comma ⇒ 〈qmsuccess,〈comma,R〉〉
+ | bit x ⇒ 〈qm1,〈mark x,L〉〉
+ | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm5 ⇒ match c with
+ [ bar ⇒ 〈qm6,〈bar,R〉〉
+ | _ ⇒ 〈qm5,〈c,R〉〉 ]
+| qm6 ⇒ match c with
+ [ bit x ⇒ 〈qm7,〈mark x,L〉〉
+ | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm7 ⇒ match c with
+ [ grid ⇒ 〈qm8,〈grid,L〉〉
+ | _ ⇒ 〈qm7,〈c,L〉〉 ]
+| qm8 ⇒ match c with
+ [ grid ⇒ 〈qm9,〈grid,R〉〉
+ | mark x ⇒ 〈qm8,〈bit x,L〉〉
+ | _ ⇒ 〈qm8,〈c,L〉〉 ]
+| qm9 ⇒ match c with
+ [ bit x ⇒ 〈qmfailure,〈mark x,L〉〉
+ | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qmsink ⇒ 〈qmsink,〈c,N〉〉
+| qmsuccess ⇒ 〈qmsuccess,〈c,N〉〉
+| qmfailure ⇒ 〈qmfailure,〈c,N〉〉].
+
+
+(*