proposition: Theorem o_proof : order term o.
proof: Proof. elim OX.o_proof; intros Rv Tv Av; elim OF.o_proof; intros Rs Ts As. unfold o; repeat split. unfold reflexive; intro t; pattern t; apply term_rec4 with (fun l => o_term_list l l = true); clear t. intros v; simpl; generalize (OX1.o_bool_ok v v); case (OX1.o_bool v v). intros _; reflexivity. intros v_not_le_v; apply False_rect; apply v_not_le_v; apply Rv. intros f l l_le_l; simpl. generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite <- o_term_list_is_o_term_list; assumption. fix o_proof 1; intro l; case l; clear l. intros _; reflexivity. intros t l H; simpl. generalize (T1.eq_bool_ok t t); case (T1.eq_bool t t); [intros _ | intro t_diff_t; apply False_rect; apply t_diff_t; reflexivity]. apply o_proof. intros; apply H; right; trivial. unfold transitive; intro t; pattern t; apply term_rec4 with (fun l1 => forall l2 l3, o_term_list l1 l2 = true -> o_term_list l2 l3 = true -> o_term_list l1 l3 = true); clear t. intros x1 t2 t3; destruct t2 as [ x2 | f2 l2 ]; destruct t3 as [ x3 | f3 l3 ]; simpl. intros x1_le_x2 x2_le_x3; assert (x1_le_x2' := OX1.o_bool_ok x1 x2); rewrite x1_le_x2 in x1_le_x2'; assert (x2_le_x3' := OX1.o_bool_ok x2 x3); rewrite x2_le_x3 in x2_le_x3'. generalize (OX1.o_bool_ok x1 x3); case (OX1.o_bool x1 x3). intros _; reflexivity. intro x1_not_le_x3; apply False_rect; apply x1_not_le_x3; apply Tv with x2; assumption. intros; discriminate. intros; discriminate. intros; discriminate. intros f1 l1 Hrec t2 t3; destruct t2 as [ x2 | f2 l2 ]; destruct t3 as [ x3 | f3 l3 ]; simpl. intros _ _; reflexivity. intros; discriminate. intros _ _; reflexivity. generalize (F.Symb.eq_bool_ok f1 f2); case (F.Symb.eq_bool f1 f2); [intro f1_eq_f2; subst f1 | intro f1_diff_f2]; (generalize (F.Symb.eq_bool_ok f2 f3); case (F.Symb.eq_bool f2 f3); [intro f2_eq_f3; subst f2 | intro f2_diff_f3]). rewrite <- o_term_list_is_o_term_list. intro l1_le_l2; rewrite <- o_term_list_is_o_term_list. intro l2_le_l3; rewrite <- o_term_list_is_o_term_list. apply Hrec with l2; assumption. intros _ f2_le_f3; assumption. intros f1_le_f3; rewrite <- o_term_list_is_o_term_list. intros l2_le_l3; rewrite <- o_term_list_is_o_term_list. generalize (F.Symb.eq_bool_ok f1 f3); case (F.Symb.eq_bool f1 f3); [intro f1_eq_f3; apply False_rect; apply f1_diff_f2 | intros _]; assumption. intros f1_le_f2 f2_le_f3; generalize (F.Symb.eq_bool_ok f1 f3); case (F.Symb.eq_bool f1 f3); [intro f1_eq_f3 | intro f1_diff_f3]. subst f3; apply False_rect; apply f1_diff_f2; apply As. generalize (OF1.o_bool_ok f1 f2); rewrite f1_le_f2; intro; assumption. generalize (OF1.o_bool_ok f2 f1); rewrite f2_le_f3; intro; assumption. generalize (OF1.o_bool_ok f1 f3); case (OF1.o_bool f1 f3); [intro f1_le_f3 | intros f1_not_le_f3]. reflexivity. apply False_rect; apply f1_not_le_f3; apply Ts with f2. generalize (OF1.o_bool_ok f1 f2); rewrite f1_le_f2; intro; assumption. generalize (OF1.o_bool_ok f2 f3); rewrite f2_le_f3; intro; assumption. fix o_proof 1; intro l1; case l1; clear l1. intros _ l2; case l2; clear l2. intros l3; case l3; clear l3. intros _ _; reflexivity. intros t2 l2 _; intros; discriminate. intros t2 l2 l3; intros; discriminate. intros t1 l1 Hrec l2; case l2; clear l2; [idtac | intros t2 l2]; (intros l3; case l3; clear l3; [idtac | intros t3 l3]; simpl). intros _ _; reflexivity. intros; discriminate. intros _ _; reflexivity. generalize (T1.eq_bool_ok t1 t2); case (T1.eq_bool t1 t2); [intro t1_eq_t2; subst t1 | intro t1_diff_t2]; (generalize (T1.eq_bool_ok t2 t3); case (T1.eq_bool t2 t3); [intro t2_eq_t3; subst t2 | intro t2_diff_t3]). apply o_proof; intros t t_in_l1; apply Hrec; right; assumption. intros _ t2_le_t3; assumption. intros t1_le_t3 l2_le_l3; generalize (T1.eq_bool_ok t1 t3); case (T1.eq_bool t1 t3); [intro t1_eq_t3; apply False_rect; apply t1_diff_t2; apply t1_eq_t3 | intros _; assumption]. intros t1_le_t2 t2_le_t3; generalize (T1.eq_bool_ok t1 t3); case (T1.eq_bool t1 t3); [intro t1_eq_t3 | intros t1_diff_t3]. subst t3; apply False_rect; apply t1_diff_t2. apply o_anti_sym; assumption. apply Hrec with t2; trivial; left; reflexivity. intros t1 t2; apply o_anti_sym. Qed.
imports: Coq(Relations List) CoLoR(list_sort term_spec)