(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

Require Import Words.

Inductive B0 : word -> Set := 
 | B0_e : B0 Eps
 | B0_ab : forall u v w, B0 (u @ v @ w) -> B0 (u :: a @ v :: b @ w)
 | B0_ba : forall u v w, B0 (u @ v @ w) -> B0 (u :: b @ v :: a @ w)
.

Inductive B1 : word -> Set := 
 | B1_e : B1 Eps
 | B1_ab : forall u v, B1 (u @ v) -> B1 (u :: a @ v :: b)
 | B1_ba : forall u v, B1 (u @ v) -> B1 (u :: b @ v :: a)
.


(*
B1_ind
     : forall P : word -> Prop,
       P Eps ->
       (forall u v : word, B1 (u @ v) -> P (u @ v) -> P (u :: a @ v :: b)) ->
       (forall u v : word, B1 (u @ v) -> P (u @ v) -> P (u :: b @ v :: a)) ->
       forall u : word, B1 u -> P u
*)

Inductive B2 : word -> Set := 
 | B2_e : B2 Eps
 | B2_ab : forall u v, B2 u -> B2 v -> B2 (u :: a @ v :: b)
 | B2_ba : forall u v, B2 u -> B2 v -> B2 (u :: b @ v :: a)
.