(* File generated by code in ../permutation/prolog/bet_permut_non_refl.pl. *)
Require Import Arith Arith.Bool_nat Omega List.
Require Import endofun permut cut.

Definition is_permutb n f := andb (is_endob n f) (is_injb n f).

(* Validation of is_permut with a non-reflexive proof. *)
Goal is_permut 1 (list2fun (0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0). omega. 
assert (y = 0). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 2 (list2fun (1::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1). omega. 
assert (y = 0 \/ y = 1). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 2 (list2fun (0::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1). omega. 
assert (y = 0 \/ y = 1). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (2::1::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (2::0::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (1::2::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (1::0::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (0::2::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 3 (list2fun (0::1::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2). omega. 
assert (y = 0 \/ y = 1 \/ y = 2). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::2::1::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::2::0::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::1::2::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::1::0::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::0::2::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (3::0::1::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::3::1::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::3::0::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::1::3::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::1::0::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::0::3::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (2::0::1::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::3::2::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::3::0::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::2::3::0::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::2::0::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::0::3::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (1::0::2::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::3::2::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::3::1::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::2::3::1::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::2::1::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::1::3::2::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.
Goal is_permut 4 (list2fun (0::1::2::3::nil)). unfold is_permut. unfold list2fun. split.
- unfold is_endo. intros x Hx. assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3).
 omega. firstorder; subst; simpl; omega.
- unfold is_inj. intros x y Hx Hy Hxy.
assert (x = 0 \/ x = 1 \/ x = 2 \/ x = 3). omega. 
assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3). omega. 
firstorder; subst; simpl; omega. Qed.



(* Time: 2 ms *)