(* File generated by code in ../permutation/prolog/bet_permut.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).

(* Test suite 1: Validation of is_permut with a reflexive proof. *)
Goal is_permut 1 (list2fun (0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 2 (list2fun (1::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 2 (list2fun (0::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (2::1::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (2::0::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (1::2::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (1::0::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (0::2::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 3 (list2fun (0::1::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::2::1::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::2::0::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::1::2::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::1::0::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::0::2::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (3::0::1::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::3::1::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::3::0::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::1::3::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::1::0::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::0::3::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (2::0::1::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::3::2::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::3::0::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::2::3::0::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::2::0::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::0::3::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (1::0::2::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::3::2::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::3::1::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::2::3::1::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::2::1::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::1::3::2::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.
Goal is_permut 4 (list2fun (0::1::2::3::nil)).
apply is_permut_dec. simpl. reflexivity. Qed.


(* Test suite 2: Validation that insertion preserves permutations (lemma insert_permut). *)
Eval compute in (is_permutb 1 (insert_fun 0 (list2fun (nil)) 0)).
Eval compute in (is_permutb 2 (insert_fun 1 (list2fun (0::nil)) 0)).
Eval compute in (is_permutb 2 (insert_fun 1 (list2fun (0::nil)) 1)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (1::0::nil)) 0)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (1::0::nil)) 1)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (1::0::nil)) 2)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (0::1::nil)) 0)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (0::1::nil)) 1)).
Eval compute in (is_permutb 3 (insert_fun 2 (list2fun (0::1::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::1::0::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::1::0::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::1::0::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::1::0::nil)) 3)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::0::1::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::0::1::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::0::1::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (2::0::1::nil)) 3)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::2::0::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::2::0::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::2::0::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::2::0::nil)) 3)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::0::2::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::0::2::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::0::2::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (1::0::2::nil)) 3)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::2::1::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::2::1::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::2::1::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::2::1::nil)) 3)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::1::2::nil)) 0)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::1::2::nil)) 1)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::1::2::nil)) 2)).
Eval compute in (is_permutb 4 (insert_fun 3 (list2fun (0::1::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::1::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::1::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::1::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::1::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::1::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::0::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::0::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::0::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::0::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::2::0::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::2::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::2::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::2::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::2::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::2::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::0::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::0::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::0::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::0::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::1::0::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::2::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::2::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::2::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::2::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::2::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::1::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::1::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::1::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::1::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (3::0::1::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::1::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::1::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::1::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::1::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::1::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::0::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::0::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::0::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::0::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::3::0::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::3::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::3::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::3::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::3::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::3::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::0::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::0::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::0::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::0::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::1::0::3::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::3::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::3::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::3::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::3::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::3::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::1::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::1::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::1::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::1::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (2::0::1::3::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::2::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::2::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::2::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::2::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::2::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::0::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::0::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::0::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::0::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::3::0::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::3::0::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::3::0::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::3::0::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::3::0::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::3::0::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::0::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::0::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::0::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::0::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::2::0::3::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::3::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::3::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::3::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::3::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::3::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::2::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::2::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::2::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::2::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (1::0::2::3::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::2::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::2::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::2::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::2::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::2::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::1::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::1::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::1::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::1::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::3::1::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::3::1::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::3::1::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::3::1::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::3::1::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::3::1::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::1::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::1::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::1::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::1::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::2::1::3::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::3::2::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::3::2::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::3::2::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::3::2::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::3::2::nil)) 4)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::2::3::nil)) 0)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::2::3::nil)) 1)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::2::3::nil)) 2)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::2::3::nil)) 3)).
Eval compute in (is_permutb 5 (insert_fun 4 (list2fun (0::1::2::3::nil)) 4)).


(* Test suite 3: Validation that direct sum preserves permutations (lemma sum_permut). *)
Eval compute in (is_permutb 0 (sum_fun 0 (list2fun (nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 1 (sum_fun 0 (list2fun (nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 1 (sum_fun 1 (list2fun (0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 2 (sum_fun 0 (list2fun (nil)) 2 (list2fun (1::0::nil)) )).
Eval compute in (is_permutb 2 (sum_fun 0 (list2fun (nil)) 2 (list2fun (0::1::nil)) )).
Eval compute in (is_permutb 2 (sum_fun 1 (list2fun (0::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 2 (sum_fun 2 (list2fun (1::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 2 (sum_fun 2 (list2fun (0::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (2::1::0::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (2::0::1::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (1::2::0::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (1::0::2::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (0::2::1::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 0 (list2fun (nil)) 3 (list2fun (0::1::2::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 1 (list2fun (0::nil)) 2 (list2fun (1::0::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 1 (list2fun (0::nil)) 2 (list2fun (0::1::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 2 (list2fun (1::0::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 2 (list2fun (0::1::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (2::1::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (2::0::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (1::2::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (1::0::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (0::2::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 3 (sum_fun 3 (list2fun (0::1::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::2::1::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::2::0::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::1::2::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::1::0::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::0::2::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (3::0::1::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::3::1::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::3::0::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::1::3::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::1::0::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::0::3::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (2::0::1::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::3::2::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::3::0::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::2::3::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::2::0::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::0::3::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (1::0::2::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::3::2::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::3::1::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::2::3::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::2::1::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::1::3::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 0 (list2fun (nil)) 4 (list2fun (0::1::2::3::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (2::1::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (2::0::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (1::2::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (1::0::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (0::2::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 1 (list2fun (0::nil)) 3 (list2fun (0::1::2::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 2 (list2fun (1::0::nil)) 2 (list2fun (1::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 2 (list2fun (1::0::nil)) 2 (list2fun (0::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 2 (list2fun (0::1::nil)) 2 (list2fun (1::0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 2 (list2fun (0::1::nil)) 2 (list2fun (0::1::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (2::1::0::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (2::0::1::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (1::2::0::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (1::0::2::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (0::2::1::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 3 (list2fun (0::1::2::nil)) 1 (list2fun (0::nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::2::1::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::2::0::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::1::2::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::1::0::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::0::2::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (3::0::1::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::3::1::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::3::0::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::1::3::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::1::0::3::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::0::3::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (2::0::1::3::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::3::2::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::3::0::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::2::3::0::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::2::0::3::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::0::3::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (1::0::2::3::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::3::2::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::3::1::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::2::3::1::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::2::1::3::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::1::3::2::nil)) 0 (list2fun (nil)) )).
Eval compute in (is_permutb 4 (sum_fun 4 (list2fun (0::1::2::3::nil)) 0 (list2fun (nil)) )).

(* Time: 5 ms *)