proposition: Theorem G_eill_complete_bound x : [< map (fun c => !⦑c⦒) Σ ++ map £ Γ |- £ x >] vec_zero -> Σ; Γ ⊦ x.
proof: Proof. Proof using w_surj. intros H. do 2 red in H. destruct (@Hrx Γ) as (v & Hv). 1: { intros ? ?; apply in_or_app; right; auto. } apply in_geill_perm with (1 := Permutation_sym Hv). fold (s x v). rewrite <- (vec_zero_plus v), vec_add_comm. apply H. rewrite ill_tps_app. exists vec_zero, v. repeat split; auto; try (rew vec; fail). 2:{ apply ill_tps_perm with (map £ (vec_map_list v (fun p => rx p))). apply Permutation_map, Permutation_sym; auto. apply ill_tps_vec_map_list_mono; auto. intros p. red. rewrite vec_map_list_one. apply in_geill_ax. } rewrite <- map_map. apply ill_tps_list_bang_zero. intros A HA. apply in_map_iff in HA. destruct HA as (c & H1 & H2); subst. destruct c as [ a p q | a p q | p q r ]; simpl. + intros y Hy; rew vec; unfold s. apply in_geill_inc with a p; auto. destruct (@Hrx (a::nil)) as (z & Hz). intros ? [ [] | [] ]; apply in_or_app; left. * apply in_flat_map; exists (LL_INC a p q); simpl; auto. * apply in_geill_perm with (vec_map_list (vec_plus z y) rx). - apply Permutation_trans with (1 := vec_map_list_plus _ _ _). change (a::vec_map_list y rx) with ((a::nil)++vec_map_list y rx). apply Permutation_app; auto. apply Permutation_sym; auto. - apply Hy; red. apply in_geill_perm with (1 := Hz), in_geill_ax. + intros u Hu y Hy. rew vec. rewrite vec_add_comm. apply in_geill_perm with (1 := Permutation_sym (vec_map_list_plus _ _ _)). apply in_geill_dec with a p; auto. + intros u (H3 & H4). rew vec. apply in_geill_fork with p q; auto. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill)