Require Import Bool.
Require Import Words.
Require Import Alternate.
Require Import Opposite.
Require Import Paired.


Inductive shuffle : word → word → word → Prop :=
  | shuffle_empty : shuffle empty empty empty
  | shuffle_bit_left :
      ∀ u v w : word,
      shuffle u v w → ∀ b : bool, shuffle (bit b u) v (bit b w)
  | shuffle_bit_right :
      ∀ u v w : word,
      shuffle u v w → ∀ b : bool, shuffle u (bit b v) (bit b w).


Lemma Shuffling :
 ∀ u v w : word,
 shuffle u v w →
 ∀ b : bool,
 alt b u →
 odd u ∧
 (odd v ∧ (alt (negb b) v → paired w) ∧ (alt b v → paired_bet b w) ∨
  even v ∧
  (alt b v → paired_odd_l b w) ∧
  (alt (negb b) v → paired_odd_r (negb b) w)) ∨
 even u ∧
 (odd v ∧
  (alt (negb b) v → paired_odd_r b w) ∧ (alt b v → paired_odd_l b w) ∨
  even v ∧ (alt b v → paired_rot b w) ∧ (alt (negb b) v → paired w)).
Proof.
simple induction 1; intros.
right.
split; auto.
right.
split; auto.
split; intro.
apply paired_rot_empty.
apply paired_empty.
elim (alt_eq b0 b u0); trivial.
elim (H1 (negb b0)); intros.
right.
elim H3; intros.
split; auto.
elim H5; intros.
elim H6; intros.
left.
elim H8; intros.
split; auto.
split; intro.
apply paired_odd_r_from_bet; auto.
apply paired_odd_l_intro; apply H9; rewrite (negb_elim b0); auto.
elim H6; intros.
elim H8; intros.
right.
split; auto.
split; intro.
apply paired_rot_bit; rewrite (negb_intro b0); apply H10;
 rewrite (negb_elim b0); auto.
apply paired_odd_l_elim; auto.
left.
elim H3; intros.
split; auto.
elim H5; intros.
left.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
apply paired_odd_l_elim; auto.
apply paired_bet_bit; apply H9; rewrite (negb_elim b0); auto.
right.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
apply paired_odd_l_intro; apply H10; rewrite (negb_elim b0); auto.
pattern b0 at 2 in |- *; rewrite (negb_intro b0).
apply paired_odd_r_from_rot; auto.
apply alt_neg_intro with b; trivial.
elim (H1 b0); intros.
left.
elim H3; intros.
split; auto.
elim H5; intros.
right.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
elim (alt_eq b0 b v0); trivial.
apply paired_odd_l_intro; apply H9; apply alt_neg_intro with b; auto.
elim (alt_eq (negb b0) b v0); trivial.
apply paired_odd_r_from_bet; rewrite (negb_elim b0); apply H10;
 apply alt_neg_elim with b; auto.
left.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
apply paired_odd_l_elim.
elim (alt_eq (negb b0) b v0); trivial.
rewrite (negb_elim b0).
apply H9.
rewrite (negb_intro b0).
apply alt_neg_intro with b; auto.
elim (alt_eq b0 b v0); trivial.
apply paired_bet_bit; apply H10; apply alt_neg_intro with b; auto.
right.
elim H3; intros.
split; auto.
elim H5; intros.
right.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
elim (alt_eq b0 b v0); trivial.
apply paired_rot_bit; apply H9; apply alt_neg_intro with b; auto.
elim (alt_eq (negb b0) b v0); trivial.
apply paired_odd_l_elim.
rewrite (negb_elim b0); apply H10; rewrite (negb_intro b0);
 apply alt_neg_intro with b; auto.
left.
elim H6; intros.
elim H8; intros.
split; auto.
split; intro.
elim (alt_eq (negb b0) b v0); trivial.
apply paired_odd_r_from_rot; apply H9; rewrite (negb_intro b0);
 apply alt_neg_intro with b; auto.
elim (alt_eq b0 b v0); trivial.
apply paired_odd_l_intro; apply H10; apply alt_neg_intro with b; auto.
trivial.
Qed.