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

Require Import Words.
Require Import BalancedWords.
Require Import GenericTactics. 
   
(* Correctness of B0 *)
Theorem B0_corr : forall u, B0 u -> |u|a = |u|b.
induction 1; splitsolve0 0. 
Qed.

(* Correctness of B1 *)
Theorem B1_corr : forall u, B1 u -> |u|a = |u|b.
induction 1; splitsolve0 0. 
Qed.

(* Correctness of B2 *)
Theorem B2_corr : forall u, B2 u -> |u|a = |u|b.
induction 1; splitsolve0 0. 
Qed.

(* B1 entails B0 *)
Theorem B1_B0 : forall u, B1 u -> B0 u.
generalize (fun u v => B0_ab u v Eps) (fun u v => B0_ba u v Eps).
intros H1 H2.
induction 1; splitsolve0 1%nat.
Qed.