proposition: Theorem ill_tps_sound Γ A : Γ ⊢ A -> [< Γ |- A >] vec_zero.
proof: Proof. induction 1 as [ A | Γ Δ A B H1 IH1 H2 IH2 | Γ Δ A H1 H2 IH2 | Γ Δ A B C H1 IH1 H2 IH2 | Γ A B H1 IH1 | Γ A B C H1 IH1 | Γ A B C H1 IH1 | Γ A B H1 IH1 H2 IH2 | Γ A B H1 IH1 | Γ A H1 IH1 | Γ A B H1 IH1 | Γ A B H1 IH1 | Γ A B C H1 IH1 | Γ Δ A B H1 IH1 H2 IH2 | Γ A B C H1 IH1 H2 IH2 | Γ A B H1 IH1 | Γ A B H1 IH1 | Γ A | Γ | Γ A H1 IH1 | ]; unfold ill_sequent_tps in * |- *. + intros x; simpl; intros (a & b & H1 & H2 & H3); subst; eq goal H2. f_equal; do 2 rewrite vec_add_comm, vec_zero_plus; auto. + intros x Hx. rewrite ill_tps_app in Hx. apply IH2. destruct Hx as (a & b & G1 & G2 & G3); subst. exists a, b; split; auto. split; auto. rewrite <- vec_zero_plus, vec_add_comm. apply IH1; auto. + revert IH2; apply ill_perm_tps; auto. + intros x (y & z & H3 & H4 & H5); simpl. apply IH2. apply ill_tps_app in H5. destruct H5 as (g & d & H5 & H6 & H7). simpl in H4. apply IH1, H4 in H6. exists (vec_plus y g), d; repeat split; auto. * subst; apply vec_add_assoc. * eq goal H6; f_equal; rew vec. + simpl; intros y Hy a Ha. rewrite vec_add_assoc. apply IH1. exists a, y; repeat split; auto; lia. + intros x (a & b & H2 & H3 & H4); apply IH1. exists a, b; repeat split; auto; apply H3. + intros x (a & b & H2 & H3 & H4); apply IH1. exists a, b; repeat split; auto; apply H3. + intros x Hx; split. * apply IH1; auto. * apply IH2; auto. + intros x (a & g & H2 & H3 & H4). apply IH1; exists a, g; repeat split; auto. apply H3. + intros x Hx; split. apply IH1; auto. rew vec. apply ill_tps_lbang in Hx; tauto. + intros x (a & g & H2 & H3 & H4). apply IH1. apply proj2 in H3; subst; auto. rew vec; auto. + intros x (a & g & H2 & H3 & H4). apply IH1. exists a, g. repeat (split; auto). exists a, g. repeat (split; auto). apply proj2 in H3. subst; rew vec; auto. + intros x Hx. apply IH1. destruct Hx as (c & g & ? & (a & b & ? & H2 & H3) & H4); subst. exists a, (vec_plus b g); split; auto. * rewrite vec_add_assoc; trivial. * split; auto; exists b, g; auto. + intros x Hx. apply ill_tps_app in Hx. destruct Hx as (a & b & ? & H3 & H4); subst. exists a, b; split. * rewrite vec_add_comm, vec_zero_plus; auto. * split; rewrite <- vec_zero_plus, vec_add_comm. - apply IH1; auto. - apply IH2; auto. + intros x Hx. destruct Hx as (u & g & ? & [ G1 | G1 ] & G2); subst. * apply IH1; exists u, g; auto. * apply IH2; exists u, g; auto. + intros x Hx; left; apply IH1; auto. + intros x Hx; right; apply IH1; auto. + intros ? (? & _ & _ & [] & _). + intros x _; red; trivial. + intros x (i & g & ? & H2 & H3); subst. red in H2; subst. rewrite vec_zero_plus. apply IH1; auto. + intros x Hx; red in Hx; subst. rewrite vec_zero_plus; red; trivial. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL)