proposition: Lemma length_check_eq: forall bs1 bs2 bsres, check_eq bs1 bs2 bsres = true -> length bs1 = length bs2.
proof: Proof. intro bs1. induction bs1. + intros. case bs2 in *. trivial. simpl in H. now contradict H. + intros. case bs2 in *. - simpl in H. now contradict H. - simpl. apply f_equal. simpl in H. revert H. case bsres. easy. intros r rl. case rl. case (Lit.is_pos r). case (t_form .[ Lit.blit r]); try easy. intro a0. case bs1 in *; try easy; case bs2; try easy. case bs1 in *; try easy; case bs2; try easy. case bs1 in *; try easy; case bs2; try easy. case bs1 in *; try easy; case bs2; try easy. case bs1 in *; try easy; case bs2; try easy. case bs1 in *; try easy; case bs2; try easy. intros i1 l a0. case (to_list a0); try easy. intros i2 l0. case (Lit.is_pos i2); try easy. case (t_form .[ Lit.blit i2]); try easy. intros i3 i4. case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros _ _ i2 l0 a0. case (to_list a0); try easy. intros i1 l. case (Lit.is_pos i1); try easy. case (t_form .[ Lit.blit i1]); try easy. intros i3 i4. case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros i2 l0 a0. case (to_list a0); try easy. intros i9 l. case (Lit.is_pos i9); try easy. case (t_form .[ Lit.blit i9]); try easy. intros i3 i4. case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. intros _ _ i2 l0 a0. case (to_list a0); try easy. intros i9 l. case (Lit.is_pos i9); try easy. case (t_form .[ Lit.blit i9]); try easy. intros i3 i4. case ((i3 =? a) && (i4 =? i) || (i3 =? i) && (i4 =? a)). apply IHbs1. easy. case bs1; try easy; case bs2; easy. case bs1; try easy; case bs2; easy. case bs1; try easy; case bs2; easy. case bs1; try easy; case bs2. simpl. easy. intros i0 l i1 i2. case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy. simpl. intros _ l i1 i2. case ((i1 =? a) && (i2 =? i) || (i1 =? i) && (i2 =? a)); easy. easy. case bs1 in *; try easy; case bs2; easy. case bs1 in *; try easy; case bs2; easy. case bs1 in *; try easy; case bs2; easy. case bs1 in *; try easy; case bs2; try easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. simpl. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)); easy. case (Lit.is_pos r); try easy. case (t_form .[ Lit.blit r]); try easy. intros x y. case ((x =? a) && (y =? i) || (x =? i) && (y =? a)). intros x2 rbs2 xr rbrs. apply IHbs1. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance