Set Implicit Arguments. Unset Strict Implicit. (* Require Export ord. *) Require Export ord. Module Uple. Export Naturals. Export Universe. (** An uple is a list indexed by natural numbers, which we view as a function whose domain is a natural number. The domain is the length, and the valid indices are all those which are strictly less than the length (starting with [0]). *) Definition axioms a := Function.axioms a & inc (domain a) nat. Definition length a := Bnat (domain a). Definition create (f:nat -> E) (l:nat) := Function.create (R l) (fun x => f (Bnat x)). Lemma domain_create : forall f l, domain (create f l) = R l. Proof. ir. uf create. rw Function.create_domain. tv. Qed. Lemma length_create : forall f l, length (create f l) = l. Proof. ir. uf length. rw domain_create. rww Bnat_R. Qed. Definition component (i:nat) a := V (R i) a. Lemma component_create : forall f l i, i < l -> component i (create f l) = f i. Proof. ir. uf component. wri inc_lt H. uf create. rw create_V_rewrite. rw Bnat_R. tv. am. Qed. Lemma create_axioms : forall f l, axioms (create f l). Proof. ir. uhg; ee. uf create. ap Function.create_axioms. rw domain_create. ap R_inc. Qed. Lemma eq_create : forall a, axioms a -> a = create (fun i => component i a) (length a). Proof. ir. cp H. uh H; ee. cp (Function.create_recovers H). transitivity (Function.create (domain a) (fun x : E => V x a)). sy; am. uf create. uf length. rw R_Bnat. ap Function.create_extensionality. tv. ir. uf component. rw R_Bnat. tv. assert (sub (domain a) nat). assert (domain a = R (B H1)). rww B_eq. rw H5. ap sub_R_nat. app H5. am. Qed. Lemma compare_create : forall f g l m, l = m -> (forall i, Peano.lt i l -> f i = g i) -> create f l = create g m. Proof. ir. wr H. uf create. ap Function.create_extensionality. tv. ir. ap H0. wr inc_lt. rww R_Bnat. ap inc_nat_from_inc_R. sh l. am. Qed. Lemma domain_emptyset : domain emptyset = emptyset. Proof. uf domain; ap extensionality; uhg; ir. rwi Image.inc_rw H. nin H. ee. nin H. elim x1. nin H. elim x0. Qed. Lemma empty_axioms : axioms emptyset. Proof. ir. uhg; ee. set (k:= Function.identity emptyset). apply sub_axioms with k. uf k. ap Function.identity_axioms. uhg; ir. nin H. elim x0. rw domain_emptyset. wr nat_zero_emptyset. ap R_inc. Qed. Lemma length_emptyset : length emptyset = 0. Proof. uf length. rw domain_emptyset. wr nat_zero_emptyset. rw Bnat_R. tv. Qed. Lemma create_length_zero : forall f , create f 0 = emptyset. Proof. ir. cp (eq_create empty_axioms). rw H. ap compare_create. rww length_emptyset. ir. cp lt_n_O. elim (H1 i H0). Qed. Lemma uple_extensionality : forall a b, axioms a -> axioms b -> length a = length b -> (forall i, i < (length a) -> component i a = component i b) -> a=b. Proof. ir. cp (eq_create H). cp (eq_create H0). rw H3; rw H4. ap compare_create. am. am. Qed. Definition concatenate a b := create (fun i => Y (i < (length a)) (component i a) (component (i - (length a)) b)) ((length a) + (length b)). Lemma length_concatenate : forall a b, length (concatenate a b) = (length a) + (length b). Proof. ir. uf concatenate. rww length_create. Qed. Lemma concatenate_axioms : forall a b, axioms (concatenate a b). Proof. ir. uf concatenate. ap create_axioms. Qed. Lemma component_concatenate_first : forall a b i, i < (length a) -> component i (concatenate a b) = component i a. Proof. ir. uf concatenate. rw component_create. rw Y_if_rw. tv. am. auto with arith. Qed. Lemma component_concatenate_second : forall a b i, i < (plus (length a) (length b)) -> (length a) <= i -> component i (concatenate a b) = component (i - (length a)) b. Proof. ir. uf concatenate. rw component_create. rw Y_if_not_rw. tv. auto with arith. am. Qed. Lemma component_concatenate_plus : forall a b i, i < (length b) -> component ((length a) + i ) (concatenate a b) = component i b. Proof. ir. rw component_concatenate_second. rw minus_plus. tv. assert (i+length a = length a + i). auto with arith. auto with arith. auto with arith. Qed. Lemma concatenate_emptyset_left : forall a, axioms a -> concatenate emptyset a = a. Proof. ir. ap uple_extensionality. ap concatenate_axioms. am. rw length_concatenate. rw length_emptyset. auto with arith. ir. rw component_concatenate_second. rw length_emptyset. assert (i- 0 = i). auto with arith. rww H1. rwi length_concatenate H0. am. rw length_emptyset. auto with arith. Qed. Lemma concatenate_emptyset_right : forall a, axioms a -> concatenate a emptyset = a. Proof. ir. ap uple_extensionality. ap concatenate_axioms. am. rw length_concatenate. rw length_emptyset. auto with arith. ir. rw component_concatenate_first. tv. rwi length_concatenate H0. rwi length_emptyset H0. assert (length a + 0 = length a). auto with arith. wrr H1. Qed. Lemma concatenate_assoc : forall a b c, concatenate a (concatenate b c) = concatenate (concatenate a b) c. Proof. ir. ap uple_extensionality. ap concatenate_axioms. ap concatenate_axioms. rw length_concatenate. rw length_concatenate. rw length_concatenate. rw length_concatenate. auto with arith. ir. apply by_cases with (i < length a + length b); ir. apply by_cases with (i x) 1. Lemma uple1_axioms : forall x, axioms (uple1 x). Proof. ir. uf uple1. ap create_axioms. Qed. Lemma length_uple1 : forall x, length (uple1 x) = 1. Proof. ir. uf uple1. rww length_create. Qed. Lemma component_uple1 : forall x i, i < 1 -> component i (uple1 x) = x. Proof. ir. uf uple1. rw component_create. tv. am. Qed. Lemma eq_uple1 : forall a x, axioms a -> length a = 1 -> x = component 0 a -> a = uple1 x. Proof. ir. rw H1. ap uple_extensionality. am. ap uple1_axioms. rw length_uple1. am. ir. rw component_uple1. assert (i=0). om. rww H3. om. Qed. Definition utack x a := concatenate a (uple1 x). Lemma utack_axioms : forall a x, axioms a -> axioms (utack x a). Proof. ir. uf utack. ap concatenate_axioms. Qed. Lemma length_utack : forall a x, axioms a -> length (utack x a) = (length a) + 1. Proof. ir. uf utack. rw length_concatenate. rww length_uple1. Qed. Lemma domain_R_length : forall a, axioms a -> domain a = R (length a). Proof. ir. uf length. rw R_Bnat. tv. uh H; ee. am. Qed. Lemma inc_R_domain : forall a i, axioms a -> inc (R i) (domain a) = (i < (length a)). Proof. ir. rw domain_R_length. rw inc_lt. tv. am. Qed. Lemma component_utack_old : forall a x i, axioms a -> i < (length a) -> component i (utack x a) = component i a. Proof. ir. uf utack. rw component_concatenate_first. tv. am. Qed. Lemma component_utack_new : forall a x i, axioms a -> i = length a -> component i (utack x a) = x. Proof. ir. uf utack. rw component_concatenate_second. rw H0. rw component_uple1. tv. wr minus_n_n. auto with arith. rw length_uple1. rw H0. assert (length a + 1 = S (length a)). rw plus_comm. auto with arith. rw H1. ap lt_n_Sn. rw H0. auto with arith. Qed. Definition restrict a i := create (fun j => component j a) i. Lemma length_restrict : forall a i, length (restrict a i) = i. Proof. ir. uf restrict. rw length_create. tv. Qed. Lemma component_restrict : forall a i j, j < i -> component j (restrict a i) = component j a. Proof. ir. uf restrict. rw component_create. tv. am. Qed. Lemma restrict_axioms : forall a i, axioms (restrict a i). Proof. ir. uf restrict. ap create_axioms. Qed. Lemma eq_utack_restrict : forall a, axioms a -> length a > 0 -> a = utack (component (length a - 1) a) (restrict a (length a -1)). Proof. ir. ap uple_extensionality. am. ap utack_axioms. ap restrict_axioms. rw length_utack. rw length_restrict. om. ap restrict_axioms. ir. assert (i = length a - 1 \/ i < length a -1). om. nin H2. rw H2. rw component_utack_new. tv. ap restrict_axioms. rw length_restrict. tv. rw component_utack_old. rw component_restrict. tv. am. ap restrict_axioms. rw length_restrict. am. Qed. Definition uple_map (f:E ->E) u := Uple.create (fun i => f (component i u)) (length u). Lemma length_uple_map : forall f u, length (uple_map f u) = length u. Proof. ir. uf uple_map. rw length_create. tv. Qed. Lemma component_uple_map : forall f u i, i < length u -> component i (uple_map f u) = f (component i u). Proof. ir. uf uple_map. rw component_create. tv. am. Qed. Lemma axioms_uple_map : forall f u, axioms (uple_map f u). Proof. ir. uf uple_map. ap create_axioms. Qed. Lemma uple_map_uple1 : forall f u, uple_map f (uple1 u) = uple1 (f u). Proof. ir. ap uple_extensionality. ap axioms_uple_map. ap uple1_axioms. rww length_uple_map. rw length_uple1. rww length_uple1. ir. rwi length_uple_map H. rwi length_uple1 H. assert (i=0). om. rw H0. rw component_uple_map. rw component_uple1. rw component_uple1. tv. om. om. rw length_uple1. om. Qed. Lemma uple_map_emptyset : forall f, uple_map f emptyset = emptyset. Proof. ir. ap uple_extensionality. ap axioms_uple_map. ap Uple.empty_axioms. rww length_uple_map. ir. rwi length_uple_map H. rwi length_emptyset H. assert (0=1). om. discriminate H0. Qed. Lemma uple_map_concatenate : forall f u v, uple_map f (concatenate u v) = concatenate (uple_map f u) (uple_map f v). Proof. ir. ap uple_extensionality. ap axioms_uple_map. ap concatenate_axioms. rw length_uple_map. rw length_concatenate. rw length_concatenate. rw length_uple_map. rw length_uple_map. tv. ir. rwi length_uple_map H. rwi length_concatenate H. rw component_uple_map. assert (i < length u \/ length u <= i). om. nin H0. rw component_concatenate_first. rw component_concatenate_first. rw component_uple_map. tv. am. rw length_uple_map. am. am. rw component_concatenate_second. rw component_concatenate_second. rw length_uple_map. rw component_uple_map. tv. om. rw length_uple_map. rw length_uple_map. am. rw length_uple_map. am. am. am. rw length_concatenate. am. Qed. Lemma restrict_full_length : forall u, axioms u -> restrict u (length u) = u. Proof. ir. ap uple_extensionality. app restrict_axioms. am. rww length_restrict. ir. rwi length_restrict H0. rww component_restrict. Qed. Lemma restrict_zero : forall u, restrict u 0 = emptyset. Proof. ir. ap uple_extensionality. app restrict_axioms. app empty_axioms. rww length_restrict. rww length_emptyset. ir. rwi length_restrict H. assert False. om. elim H0. Qed. Definition coincide_before a b i := Uple.axioms a & Uple.axioms b & i <= length a & i <= length b & (forall j, j < i -> component j a = component j b). Lemma coincide_restrict_rw : forall a b i, Uple.axioms a -> Uple.axioms b -> i <= length a -> i <= length b -> (coincide_before a b i = (restrict a i = restrict b i)). Proof. ir. ap iff_eq; ir. ap uple_extensionality. app restrict_axioms. app restrict_axioms. rw length_restrict. rww length_restrict. ir. rwi length_restrict H4. rw component_restrict. rw component_restrict. uh H3; ee. ap H8. am. am. am. uhg; ee; try am. ir. transitivity (component j (restrict a i)). rww component_restrict. rw H3. rww component_restrict. Qed. Lemma coincide_before_leq : forall a b j, (exists i, (coincide_before a b i & j <= i)) -> coincide_before a b j. Proof. ir. nin H. ee. uh H; ee. uhg; ee; try am. om. om. ir. ap H4. om. Qed. Lemma coincide_before_trans : forall a c i, (exists b, (coincide_before a b i & coincide_before b c i)) -> coincide_before a c i. Proof. ir. induction H as [b]. ee. uh H; uh H0; ee. uhg; ee; try am. ir. rww H8. app H4. Qed. Lemma coincide_before_refl : forall a i, Uple.axioms a -> i<= length a -> coincide_before a a i. Proof. ir. uhg; ee; try am. ir. tv. Qed. Lemma coincide_before_symm : forall a b i, coincide_before a b i -> coincide_before b a i. Proof. ir. uh H; ee. uhg; ee; try am. ir. sy; au. Qed. Lemma coincide_before_symm_rw : forall a b i, coincide_before a b i = coincide_before b a i. Proof. ir. ap iff_eq; ir; app coincide_before_symm. Qed. Lemma nonemptyT_nat : nonemptyT nat. Proof. sh 0. Qed. Ltac ind H a := induction H as [a]. Definition nat_prop_smallest p i := (p i) & (forall j, p j -> i <= j). Lemma excluded_middle_or : forall (p:Prop), p \/ ~ p. Proof. ir. apply excluded_middle. uhg; ir. assert p. apply excluded_middle. uhg; ir. ap H. ap or_intror. am. ap H. ap or_introl. am. Qed. Lemma ex_nat_prop_smallest : forall i (p:nat -> Prop), p i -> ex (nat_prop_smallest p). Proof. intro i. induction i. ir. sh 0. uhg; ee. am. ir. om. ir. cp (IHi (fun j=> p (S j)) H). ind H0 k. uh H0; ee. cp (excluded_middle_or (p 0)). nin H2. sh 0. uhg; ee. am. ir. om. sh (S k). uhg; ee. am. ir. assert (j > 0). assert (~ j = 0). uhg; ir. rwi H4 H3. app H2. om. assert (k <= j-1). ap H1. assert (S (j-1) = j). om. rw H5. am. om. Qed. Definition nat_prop_min p := chooseT (nat_prop_smallest p) nonemptyT_nat. Lemma nat_prop_smallest_nat_prop_min : forall p, ex p -> nat_prop_smallest p (nat_prop_min p). Proof. ir. uf nat_prop_min. ap chooseT_pr. ind H i. apply ex_nat_prop_smallest with i. am. Qed. Lemma p_nat_prop_min : forall p, ex p -> p (nat_prop_min p). Proof. ir. cp (nat_prop_smallest_nat_prop_min H). uh H0; ee. am. Qed. Lemma nat_prop_min_smallest : forall i (p:nat -> Prop), p i -> nat_prop_min p <= i. Proof. ir. assert (ex p). sh i; am. cp (nat_prop_smallest_nat_prop_min H0). uh H1; ee. au. Qed. Lemma nat_prop_min_eq : forall i (p:nat->Prop), p i -> (forall j, p j -> i<= j) -> nat_prop_min p = i. Proof. ir. assert (nat_prop_min p <= i). app nat_prop_min_smallest. assert (i <= nat_prop_min p). ap H0. ap p_nat_prop_min. sh i; am. om. Qed. Definition nat_prop_bounds (p:nat -> Prop) (i:nat):= (forall j, p j -> j <= i). Definition nat_prop_max p := nat_prop_min (nat_prop_bounds p). Lemma nat_prop_bounds_nat_prop_max : forall p, ex (nat_prop_bounds p) -> nat_prop_bounds p (nat_prop_max p). Proof. ir. uf nat_prop_max. app p_nat_prop_min. Qed. Lemma nat_prop_max_smallest : forall i p, nat_prop_bounds p i -> nat_prop_max p <= i. Proof. ir. uf nat_prop_max. app nat_prop_min_smallest. Qed. Lemma p_nat_prop_max : forall p, ex (nat_prop_bounds p) -> ex p -> p (nat_prop_max p). Proof. ir. ap excluded_middle. uhg; ir. assert (nat_prop_max p > 0). assert (nat_prop_max p <> 0). uhg; ir. assert (nat_prop_bounds p 0). wr H2. app nat_prop_bounds_nat_prop_max. uh H3; ee. rwi H2 H1. ind H0 i. assert (i <= 0). au. assert (i = 0). om. ap H1. wrr H5. om. assert (nat_prop_bounds p ((nat_prop_max p) -1)). cp (nat_prop_bounds_nat_prop_max H). uh H3; ee. uhg. ir. cp (H3 _ H4). assert (j <> nat_prop_max p). uhg; ir. wri H6 H1. au. om. cp (nat_prop_max_smallest H3). om. Qed. Lemma max_nat_prop_max : forall i p, ex (nat_prop_bounds p) -> p i -> i <= nat_prop_max p. Proof. ir. cp (nat_prop_bounds_nat_prop_max H). uh H1; ee. au. Qed. Lemma nat_prop_max_eq : forall i p, nat_prop_bounds p i -> p i -> nat_prop_max p = i. Proof. ir. uf nat_prop_max. app nat_prop_min_eq. ir. uh H1; ee. au. Qed. Definition coincidence a b := nat_prop_max (coincide_before a b). Lemma nat_prop_bounds_length_left : forall a b, nat_prop_bounds (coincide_before a b) (length a). Proof. ir. uhg. ir. uh H; ee. am. Qed. Lemma nat_prop_bounds_length_right : forall a b, nat_prop_bounds (coincide_before a b) (length b). Proof. ir. uhg. ir. uh H; ee. am. Qed. Lemma ex_nat_prop_bounds_coincide_before : forall a b, ex (nat_prop_bounds (coincide_before a b)). Proof. ir. sh (length a). ap nat_prop_bounds_length_left. Qed. Lemma coincide_before_zero : forall a b, Uple.axioms a -> Uple.axioms b -> coincide_before a b 0. Proof. ir. uhg; ee. am. am. om. om. ir. assert False. om. elim H2. Qed. Lemma coincide_before_coincidence : forall a b, Uple.axioms a -> Uple.axioms b -> coincide_before a b (coincidence a b). Proof. ir. uf coincidence. ap p_nat_prop_max. ap ex_nat_prop_bounds_coincide_before. sh 0. app coincide_before_zero. Qed. Lemma leq_coincidence_component_eq : forall a b i, Uple.axioms a -> Uple.axioms b -> i < coincidence a b -> component i a = component i b. Proof. ir. cp (coincide_before_coincidence H H0). uh H2; ee. app H6. Qed. Lemma leq_coincidence : forall a b i, Uple.axioms a -> Uple.axioms b -> coincide_before a b i -> i <= coincidence a b. Proof. ir. uf coincidence. app max_nat_prop_max. sh (length a). app nat_prop_bounds_length_left. Qed. Lemma coincide_before_leq_coincidence : forall a b i, Uple.axioms a -> Uple.axioms b -> coincide_before a b i = (i <= coincidence a b). Proof. ir. ap iff_eq; ir. app leq_coincidence. ap coincide_before_leq. sh (coincidence a b). ee. app coincide_before_coincidence. am. Qed. Lemma lt_coincidence_component_eq : forall a b i, Uple.axioms a -> Uple.axioms b -> i < coincidence a b -> component i a = component i b. Proof. ir. assert (coincide_before a b (coincidence a b)). app coincide_before_coincidence. uh H2; ee. au. Qed. Lemma component_coincidence_neq : forall a b, Uple.axioms a -> Uple.axioms b -> coincidence a b < length a -> coincidence a b < length b -> (component (coincidence a b) a) <> (component (coincidence a b) b). Proof. ir. uhg. ir. assert (coincide_before a b (coincidence a b +1)). uhg; ee. am. am. om. om. ir. assert (j < coincidence a b \/ j = coincidence a b). om. nin H5. app lt_coincidence_component_eq. rww H5. assert (coincidence a b + 1 <= coincidence a b). ap leq_coincidence. am. am. am. om. Qed. Lemma leq_coincidence_left : forall a b, Uple.axioms a -> Uple.axioms b -> coincidence a b <= length a. Proof. ir. uf coincidence. app nat_prop_max_smallest. app nat_prop_bounds_length_left. Qed. Lemma leq_coincidence_right : forall a b, Uple.axioms a -> Uple.axioms b -> coincidence a b <= length b. Proof. ir. uf coincidence. app nat_prop_max_smallest. app nat_prop_bounds_length_right. Qed. Definition common a b := restrict a (coincidence a b). Lemma axioms_common : forall a b, Uple.axioms (common a b). Proof. ir. uf common. app restrict_axioms. Qed. Lemma length_common : forall a b, length (common a b) = coincidence a b. Proof. ir. uf common. rww length_restrict. Qed. Lemma leq_length_common_left : forall a b, Uple.axioms a -> Uple.axioms b -> length (common a b) <= length a . Proof. ir. rw length_common. app leq_coincidence_left. Qed. Lemma leq_length_common_right: forall a b, Uple.axioms a -> Uple.axioms b -> length (common a b) <= length b . Proof. ir. rw length_common. app leq_coincidence_right. Qed. Lemma component_common_left : forall a b i, Uple.axioms a -> Uple.axioms b -> i component i (common a b) = component i a. Proof. ir. uf common. rw component_restrict. tv. am. Qed. Lemma component_common_right: forall a b i, Uple.axioms a -> Uple.axioms b -> i component i (common a b) = component i b. Proof. ir. uf common. rww component_restrict. app lt_coincidence_component_eq. Qed. Lemma coincide_before_common_left : forall a b i, Uple.axioms a -> Uple.axioms b -> i<= coincidence a b -> coincide_before a (common a b) i. Proof. ir. uhg; ee; try am. ap axioms_common. cp (leq_length_common_left H H0). rwi length_common H2. om. rww length_common. ir. rww component_common_left. om. Qed. Lemma coincide_before_common_right : forall a b i, Uple.axioms a -> Uple.axioms b -> i<= coincidence a b -> coincide_before b (common a b) i. Proof. ir. uhg; ee; try am. ap axioms_common. cp (leq_length_common_right H H0). rwi length_common H2. om. rww length_common. ir. rww component_common_right. om. Qed. Definition sub_uple a b := Uple.axioms a & Uple.axioms b & length a <= length b & restrict b (length a) = a. Lemma show_sub_uple : forall a b, Uple.axioms a -> Uple.axioms b -> length a <= length b -> (forall i, i component i a = component i b) -> sub_uple a b. Proof. ir. uhg; ee; try am. ap uple_extensionality. ap restrict_axioms. am. rww length_restrict. ir. rww component_restrict. sy. ap H2. rwi length_restrict H3. am. rwi length_restrict H3. am. Qed. Lemma component_sub_uple : forall a b i, sub_uple a b -> i component i a = component i b. Proof. ir. uh H; ee. wr H3. rw component_restrict. tv. am. Qed. Lemma sub_uple_refl : forall a, Uple.axioms a -> sub_uple a a. Proof. ir. app show_sub_uple. Qed. Lemma sub_uple_trans : forall a c, (exists b, (sub_uple a b & sub_uple b c)) -> sub_uple a c. Proof. ir. induction H as [b]. ee. uh H; uh H0; ee. app show_sub_uple. om. ir. rewrite component_sub_uple with (b:=b). ap component_sub_uple. uhg; ee; am. om. uhg; ee; am. am. Qed. Lemma sub_uple_extens : forall a b, sub_uple a b -> sub_uple b a -> a = b. Proof. ir. ap uple_extensionality. lu. lu. uh H; uh H0; ee; om. ir. ap component_sub_uple. am. am. Qed. Lemma sub_uple_common_left : forall a b, Uple.axioms a -> Uple.axioms b -> sub_uple (common a b) a. Proof. ir. ap show_sub_uple. ap axioms_common. am. app leq_length_common_left. ir. rwi length_common H1. rww component_common_left. Qed. Lemma sub_uple_common_right: forall a b, Uple.axioms a -> Uple.axioms b -> sub_uple (common a b) b. Proof. ir. ap show_sub_uple. ap axioms_common. am. app leq_length_common_right. ir. rwi length_common H1. rww component_common_right. Qed. Lemma sub_uple_rw : forall a b, sub_uple a b = coincide_before a b (length a). Proof. ir. ap iff_eq; ir. uh H; ee. uhg; ee; try am. om. ir. wr H2. rww component_restrict. uh H; ee. app show_sub_uple. Qed. Lemma common_univ_sub_uple : forall a b c, sub_uple c a -> sub_uple c b -> sub_uple c (common a b). Proof. ir. rwi sub_uple_rw H. rwi sub_uple_rw H0. rw sub_uple_rw. ap coincide_before_trans. sh a. ee. am. ap coincide_before_common_left. lu. lu. assert (coincide_before a b (length c)). ap coincide_before_trans. sh c. ee; try am. rw coincide_before_symm_rw. am. wr coincide_before_leq_coincidence. am. lu. lu. Qed. Lemma sub_uple_length_leq : forall a b, sub_uple a b -> length a <= length b. Proof. ir. lu. Qed. Lemma sub_uple_common_eq : forall a b, sub_uple a b -> common a b = a. Proof. ir. ap sub_uple_extens. app sub_uple_common_left. lu. lu. ap common_univ_sub_uple. app sub_uple_refl. lu. am. Qed. Lemma common_symm : forall a b, axioms a -> axioms b -> common a b = common b a. Proof. ir. ap sub_uple_extens. ap common_univ_sub_uple. app sub_uple_common_right. app sub_uple_common_left. ap common_univ_sub_uple. app sub_uple_common_right. app sub_uple_common_left. Qed. End Uple. Module Graph. Export Uple. Open Local Scope string_scope. Definition Vertices := R "Vertices". Definition Edges := R "Edges". Definition vertices a := V Vertices a. Definition edges a := V Edges a. Definition create v e := denote Vertices v (denote Edges e stop). Definition like a := a = create (vertices a) (edges a). Lemma vertices_create : forall v e, vertices (create v e) =v. Proof. ir; uf vertices; uf create. drw. Qed. Lemma edges_create : forall v e, edges (create v e) = e. Proof. ir; uf edges; uf create. drw. Qed. Lemma create_like : forall v e, like (create v e). Proof. ir. uf like. rw vertices_create. rw edges_create. tv. Qed. Lemma like_extensionality : forall a b, like a -> like b -> vertices a = vertices b -> edges a = edges b -> a = b. Proof. ir. uh H; uh H0. rw H ; rw H0. rw H1; rw H2. tv. Qed. Definition axioms a := like a & (forall u, inc u (edges a) -> Arrow.like u) & (forall u, inc u (edges a) -> inc (source u) (vertices a)) & (forall u, inc u (edges a) -> inc (target u) (vertices a)). Lemma axioms_extensionality : forall a b, axioms a -> axioms b -> vertices a = vertices b -> edges a = edges b -> a = b. Proof. ir. uh H; uh H0. ee. app like_extensionality. Qed. End Graph. Module Binary. Export Naturals. Definition binary b := inc b (R 2). Lemma binary_dichot : forall b, binary b = (b = (R 0) \/ b = (R 1)). Proof. ir. uf binary. ap inc_two. Qed. Lemma binary_zero : binary (R 0). Proof. rw binary_dichot. app or_introl. Qed. Lemma binary_one : binary (R 1). Proof. rw binary_dichot. app or_intror. Qed. End Binary. Module TreeIndex. Export Universe. Export Uple. Export Binary. Definition natuple p := Uple.axioms p & (forall i, i<(length p) -> inc (component i p) nat). Definition binuple p := Uple.axioms p & (forall i, i<(length p) -> binary (component i p)). Lemma binuple_rw : forall p, binuple p = (natuple p & (forall i, i<(length p) -> binary (component i p))). Proof. ir. ap iff_eq; ir. ee. uhg; ee. lu. uh H; ee. ir. cp (H0 _ H1). uh H2. assert (sub (R 2) nat). app sub_R_nat. app H3. lu. ee. uhg; ee. lu. lu. Qed. Lemma binuple_natuple : forall p, binuple p -> natuple p. Proof. ir. rwi binuple_rw H. ee; am. Qed. Definition above p := restrict p (length p - 1). Definition branch (i:nat) p := utack (R i) p. Definition underleft p := branch 0 p. Definition underright p := branch 1 p. Definition last_component p:= component (length p - 1) p. Lemma length_branch : forall i p, natuple p -> length (branch i p) = length p + 1. Proof. ir. uf branch. rww length_utack. lu. Qed. Lemma length_underleft : forall p, binuple p -> length (underleft p) = length p + 1. Proof. ir. uf underleft. rww length_branch. app binuple_natuple. Qed. Lemma length_underright : forall p, binuple p -> length (underright p) = length p + 1. Proof. ir. uf underright. rww length_branch. app binuple_natuple. Qed. Lemma natuple_above : forall p, natuple p -> natuple (above p). Proof. ir. uf above. uhg; ee. app restrict_axioms. ir. uh H; ee. rwi length_restrict H0. rww component_restrict. ap H1. om. Qed. Lemma binuple_above : forall p, binuple p -> binuple (above p). Proof. ir. assert (length p = 0 \/ length p > 0). om. nin H0. uhg; ee. uf above. app restrict_axioms. ir. assert (length (above p) = 0). uf above. rw length_restrict. rw H0. om. rwi H2 H1. assert False. om. elim H3. uhg; ee. uf above. app restrict_axioms. ir. assert (length (above p) = length p - 1). uf above. rww length_restrict. rwi H2 H1. uf above. rw component_restrict. uh H; ee. ap H3. om. am. Qed. Definition nonroot p := natuple p & length p > 0. Lemma nonroot_nonempty : forall p, nonroot p -> nonempty p. Proof. ir. uh H; ee. cp (emptyset_dichot p). nin H1. rwi H1 H0. cp length_emptyset. assert False. om. elim H3. am. Qed. Lemma root_nonroot : forall p, natuple p -> (p = emptyset \/ nonroot p). Proof. ir. cp (emptyset_dichot p). nin H0. app or_introl. ap or_intror. uhg; ee; try am. assert (length p = 0 \/ length p > 0). om. nin H1. assert (p = emptyset). apply uple_extensionality. uh H; ee. am. ap Uple.empty_axioms. rww length_emptyset. ir. rwi H1 H2. assert False. om. elim H3. rwi H2 H0. nin H0. nin H0. nin x. am. Qed. Lemma length_above : forall p, natuple p -> length (above p) = length p - 1. Proof. ir. uf above. rww length_restrict. Qed. Lemma utack_last_component : forall p, nonroot p -> utack (last_component p) (above p) = p. Proof. ir. uf last_component. uf above. sy. ap eq_utack_restrict. uh H; ee. uh H; ee. am. uh H; ee; am. Qed. Lemma binary_last_component : forall p, nonroot p -> binuple p -> binary (last_component p). Proof. ir. uf last_component. uh H; ee. uh H0; ee. ap H2. om. Qed. Lemma underleft_above : forall p, nonroot p -> last_component p = (R 0) -> underleft (above p) = p. Proof. ir. uf underleft. uf branch. wr H0. app utack_last_component. Qed. Lemma underright_above : forall p, nonroot p -> last_component p = (R 1) -> underright (above p) = p. Proof. ir. uf underright. uf branch. wr H0. app utack_last_component. Qed. Lemma under_above_dichot : forall p, nonroot p -> binuple p -> (p = underleft (above p) \/ p = underright (above p)). Proof. ir. cp (binary_last_component H H0). rwi binary_dichot H1. nin H1. ap or_introl. sy; app underleft_above. ap or_intror. sy; app underright_above. Qed. Definition on_left_edge p := binuple p & (forall i, i< length p -> component i p = R 0). Definition on_right_edge p := binuple p & (forall i, i< length p -> component i p = R 1). Lemma component_above : forall i p, i < length p -1 -> component i (above p) = component i p. Proof. ir. uf above. rww component_restrict. Qed. Lemma component_branch : forall i j p, natuple p -> i < length p -> component i (branch j p) = component i p. Proof. ir. uf branch. rww component_utack_old. lu. Qed. Lemma component_underleft : forall i p, binuple p -> i < length p -> component i (underleft p) = component i p. Proof. ir. uf underleft. rww component_branch. app binuple_natuple. Qed. Lemma component_underright : forall i p, binuple p -> i < length p -> component i (underright p) = component i p. Proof. ir. uf underright. rww component_branch. app binuple_natuple. Qed. Lemma last_component_branch : forall i p, natuple p -> last_component (branch i p) = R i. Proof. ir. uf branch. uf last_component. rw length_utack. assert (length p + 1 - 1 = length p). om. rw H0. rww component_utack_new. lu. lu. Qed. Lemma last_component_underleft : forall p, binuple p -> last_component (underleft p) = R 0. Proof. ir. uf underleft. rww last_component_branch. app binuple_natuple. Qed. Lemma last_component_underright : forall p, binuple p -> last_component (underright p) = R 1. Proof. ir. uf underright. rww last_component_branch. app binuple_natuple. Qed. Lemma component_length_branch : forall i p, natuple p -> component (length p) (branch i p) = R i. Proof. ir. cp (last_component_branch i H). ufi last_component H0. rwi length_branch H0. assert (length p + 1-1 = length p). om. rwi H1 H0. am. am. Qed. Lemma component_length_underleft : forall p, binuple p -> component (length p) (underleft p) = R 0. Proof. ir. uf underleft. rww component_length_branch. app binuple_natuple. Qed. Lemma component_length_underright : forall p, binuple p -> component (length p) (underright p) = R 1. Proof. ir. uf underright. rww component_length_branch. app binuple_natuple. Qed. Lemma natuple_branch : forall i p, natuple p -> natuple (branch i p). Proof. ir. uhg; ee. uf branch. app utack_axioms. lu. ir. rwi length_branch H0. assert (i0 < length p \/ i0 = length p). om. nin H1. uh H; ee. rw component_branch. au. uhg; ee; am. am. rw H1. rw component_length_branch. ap R_inc. am. am. Qed. Lemma binuple_underleft : forall p, binuple p -> binuple (underleft p). Proof. ir. rw binuple_rw. ee. uf underleft. app natuple_branch. app binuple_natuple. ir. rwi length_underleft H0. assert (i < length p \/ i = length p). om. nin H1. rw component_underleft. uh H; ee; au. am. am. rw H1. uf underleft. rw component_length_branch. ap binary_zero. app binuple_natuple. am. Qed. Lemma binuple_underright : forall p, binuple p -> binuple (underright p). Proof. ir. rw binuple_rw. ee. uf underright. app natuple_branch. app binuple_natuple. ir. rwi length_underright H0. assert (i < length p \/ i = length p). om. nin H1. rw component_underright. uh H; ee; au. am. am. rw H1. uf underright. rw component_length_branch. ap binary_one. app binuple_natuple. am. Qed. Lemma nonroot_branch : forall i p, natuple p -> nonroot (branch i p). Proof. ir. uf nonroot. ee. app natuple_branch. rw length_branch. om. am. Qed. Lemma nonroot_underleft : forall p, binuple p -> nonroot (underleft p). Proof. ir. uf underleft. ap nonroot_branch. app binuple_natuple. Qed. Lemma nonroot_underright : forall p, binuple p -> nonroot (underright p). Proof. ir. uf underright. ap nonroot_branch. app binuple_natuple. Qed. Lemma above_branch : forall i p, natuple p -> above (branch i p) = p. Proof. ir. uf above. uf branch. apply uple_extensionality. app restrict_axioms. uh H; ee; am. rw length_restrict. rw length_utack. om. uh H; ee; am. ir. rwi length_restrict H0. rwi length_utack H0. assert (i0< length p). om. rw component_restrict. rw component_utack_old. tv. uh H; ee; am. am. rw length_utack. am. uh H; ee; am. uh H; ee; am. Qed. Lemma above_underleft : forall p, binuple p -> above (underleft p) = p. Proof. ir. uf underleft. rww above_branch. app binuple_natuple. Qed. Lemma above_underright : forall p, binuple p -> above (underright p) = p. Proof. ir. uf underright. rww above_branch. app binuple_natuple. Qed. Lemma natuple_emptyset : natuple emptyset. Proof. ir. uhg; ee. ap empty_axioms. ir. rwi length_emptyset H. assert False. om. elim H0. Qed. Lemma binuple_emptyset : binuple emptyset. Proof. ir. uhg; ee. ap empty_axioms. ir. rwi length_emptyset H. assert False. om. elim H0. Qed. Lemma binuple_dichot : forall p, binuple p -> (p = emptyset \/ p = underleft (above p) \/ p = underright (above p)). Proof. ir. cp H. rwi binuple_rw H0. ee. cp (root_nonroot H0). nin H2. ap or_introl. am. ap or_intror. ap under_above_dichot. am. am. Qed. Lemma on_left_edge_above : forall p, on_left_edge p -> on_left_edge (above p). Proof. ir. uh H; ee. uhg; ee. app binuple_above. ir. rwi length_above H1. rww component_above. ap H0. om. app binuple_natuple. Qed. Lemma on_right_edge_above : forall p, on_right_edge p -> on_right_edge (above p). Proof. ir. uh H; ee. uhg; ee. app binuple_above. ir. rwi length_above H1. rww component_above. ap H0. om. app binuple_natuple. Qed. Lemma on_left_edge_underleft : forall p, on_left_edge p -> on_left_edge (underleft p). Proof. ir. uhg; ee. ap binuple_underleft. uh H; ee. am. ir. uh H; ee. rwi length_underleft H0. assert (i = length p \/ i < length p). om. nin H2. rw H2. rww component_length_underleft. rw component_underleft. app H1. am. am. am. Qed. Lemma on_right_edge_underright : forall p, on_right_edge p -> on_right_edge (underright p). Proof. ir. uhg; ee. ap binuple_underright. uh H; ee. am. ir. uh H; ee. rwi length_underright H0. assert (i = length p \/ i < length p). om. nin H2. rw H2. rww component_length_underright. rw component_underright. app H1. am. am. am. Qed. Definition vertical p q := natuple p & natuple q & sub_uple p q. Lemma vertical_refl : forall p, natuple p -> vertical p p. Proof. ir. uhg; ee. am. am. ap sub_uple_refl. lu. Qed. Lemma vertical_trans : forall p q r, vertical p q -> vertical q r -> vertical p r. Proof. ir. uhg; ee. lu. lu. ap sub_uple_trans. sh q. ee. lu. lu. Qed. Lemma show_vertical : forall p q, natuple p -> natuple q -> length p <= length q -> (forall i, i< length p -> component i p = component i q) -> vertical p q. Proof. ir. uhg; ee; try am. ap show_sub_uple. lu. lu. am. am. Qed. Lemma vertical_above : forall p, natuple p -> vertical (above p) p. Proof. ir. ap show_vertical. app natuple_above. am. rww length_above. om. ir. rwi length_above H0. rww component_above. am. Qed. Lemma vertical_branch : forall i p, natuple p -> vertical p (branch i p). Proof. ir. ap show_vertical. am. app natuple_branch. rww length_branch. om. ir. rww component_branch. Qed. Lemma vertical_underleft : forall p, binuple p -> vertical p (underleft p). Proof. ir. uf underleft. app vertical_branch. app binuple_natuple. Qed. Lemma vertical_underright : forall p, binuple p -> vertical p (underright p). Proof. ir. uf underright. app vertical_branch. app binuple_natuple. Qed. Lemma vertical_emptyset : forall p, natuple p -> vertical emptyset p. Proof. ir. ap show_vertical. ap natuple_emptyset. am. rw length_emptyset. om. ir. rwi length_emptyset H0. assert False. om. elim H1. Qed. Lemma vertical_extens : forall p q, vertical p q -> vertical q p -> p = q. Proof. ir. uh H; ee. uh H0; ee. ap sub_uple_extens. am. am. Qed. Lemma vertical_same_components : forall p q i, vertical p q -> i < length p -> component i p = component i q. Proof. ir. uh H; ee. uh H2; ee. wr H5. rww component_restrict. Qed. Lemma vertical_dichot : forall p q r, vertical q p -> vertical r p -> (vertical q r \/ vertical r q). Proof. ir. assert (length q <= length r \/ length r <= length q). om. nin H1. ap or_introl. ap show_vertical. lu. lu. am. ir. transitivity (component i p). app vertical_same_components. sy. app vertical_same_components. om. ap or_intror. ap show_vertical. lu. lu. am. ir. transitivity (component i p). app vertical_same_components. sy. app vertical_same_components. om. Qed. Lemma vertical_common_eq : forall p q, vertical p q -> common p q = p. Proof. ir. uh H; ee. app sub_uple_common_eq. Qed. Definition Ncomponent i p := Bnat (component i p). Lemma R_Ncomponent : forall i p, natuple p -> i < length p -> R (Ncomponent i p) = component i p. Proof. ir. uf Ncomponent. rww R_Bnat. uh H; ee; au. Qed. Lemma common_common1: forall a b, Uple.axioms a -> Uple.axioms b -> common (common a b) a = common a b. Proof. ir. ap sub_uple_common_eq. ap sub_uple_common_left. am. am. Qed. Lemma common_common2 : forall a b, Uple.axioms a -> Uple.axioms b -> common (common a b) b = common a b. Proof. ir. ap sub_uple_common_eq. ap sub_uple_common_right. am. am. Qed. Lemma natuple_common : forall p q, natuple p -> natuple q -> natuple (common p q). Proof. ir. uhg; ee. uf common. app restrict_axioms. ir. assert (length (common p q) <= length p). app leq_length_common_left. lu. lu. rw component_common_left. uh H; ee. ap H3. om. lu. lu. rwi length_common H1. am. Qed. Lemma binuple_common : forall p q, binuple p -> binuple q -> binuple (common p q). Proof. ir. uhg; ee. ap axioms_common. ir. rw component_common_left. uh H; ee. ap H2. assert (length (common p q) <= length p). rw length_common. ap leq_coincidence_left. am. lu. om. lu. lu. wrr length_common. Qed. Lemma vertical_common_left : forall p q, natuple p -> natuple q -> vertical (common p q) p. Proof. ir. uhg; ee. app natuple_common. am. app sub_uple_common_left. lu. lu. Qed. Lemma vertical_common_right : forall p q, natuple p -> natuple q -> vertical (common p q) q. Proof. ir. uhg; ee. app natuple_common. am. app sub_uple_common_right. lu. lu. Qed. Lemma natuple_extensionality: forall a b : E, natuple a -> natuple b -> length a = length b -> (forall i : nat, i < length a -> Ncomponent i a = Ncomponent i b) -> a = b. Proof. ir. ap uple_extensionality. uh H; ee. am. uh H0; ee; am. am. ir. wr R_Ncomponent. wr R_Ncomponent. rw H2. tv. am. am. wrr H1. am. am. Qed. Lemma Ncomponent_concatenate_first: forall (a b : E) (i : nat), natuple a -> natuple b -> i < length a -> Ncomponent i (concatenate a b) = Ncomponent i a. Proof. ir. assert (component i (concatenate a b) = component i a). app component_concatenate_first. uf Ncomponent. rww H2. Qed. Lemma Ncomponent_concatenate_second: forall (a b : E) (i : nat), natuple a -> natuple b -> i < length a + length b -> length a <= i -> Ncomponent i (concatenate a b) = Ncomponent (i - length a) b. Proof. ir. assert (component i (concatenate a b) = component (i - length a) b). app component_concatenate_second. uf Ncomponent. rww H3. Qed. Lemma Ncomponent_concatenate_plus: forall (a b : E) (i : nat), natuple a -> natuple b -> i < length b -> Ncomponent (length a + i) (concatenate a b) = Ncomponent i b. Proof. ir. assert (component (length a + i) (concatenate a b) = component i b). app component_concatenate_plus. uf Ncomponent. rww H2. Qed. Lemma Ncomponent_restrict: forall (a : E) (i j : nat), natuple a -> j < i -> Ncomponent j (restrict a i) = Ncomponent j a. Proof. ir. assert (component j (restrict a i) = component j a). app component_restrict. uf Ncomponent. rww H1. Qed. Lemma lt_coincidence_Ncomponent_eq: forall (a b : E) (i : nat), natuple a -> natuple b -> i < coincidence a b -> Ncomponent i a = Ncomponent i b. Proof. ir. assert (component i a = component i b). app lt_coincidence_component_eq. lu. lu. uf Ncomponent. rww H2. Qed. Lemma Ncomponent_coincidence_neq: forall a b : E, natuple a -> natuple b -> coincidence a b < length a -> coincidence a b < length b -> Ncomponent (coincidence a b) a <> Ncomponent (coincidence a b) b. Proof. ir. assert (component (coincidence a b) a <> component (coincidence a b) b). app component_coincidence_neq. lu. lu. uhg; ir. ap H3. wrr R_Ncomponent. wrr R_Ncomponent. rww H4. Qed. Lemma Ncomponent_common_left: forall (a b : E) (i : nat), natuple a -> natuple b -> i < coincidence a b -> Ncomponent i (common a b) = Ncomponent i a. Proof. ir. assert (component i (common a b) = component i a). app component_common_left. lu. lu. uf Ncomponent. rww H2. Qed. Lemma Ncomponent_common_right: forall (a b : E) (i : nat), natuple a -> natuple b -> i < coincidence a b -> Ncomponent i (common a b) = Ncomponent i b. Proof. ir. assert (component i (common a b) = component i b). app component_common_right. lu. lu. uf Ncomponent. rww H2. Qed. Definition sub_natuple p q := natuple p & natuple q & sub_uple p q. Lemma show_sub_natuple: forall a b : E, natuple a -> natuple b -> length a <= length b -> (forall i : nat, i < length a -> Ncomponent i a = Ncomponent i b) -> sub_natuple a b. Proof. ir. assert (sub_uple a b). app show_sub_uple. lu. lu. ir. cp (H2 _ H3). wrr R_Ncomponent. wrr R_Ncomponent. rww H4. om. uhg; ee; am. Qed. Lemma Ncomponent_sub_natuple: forall (a b : E) (i : nat), sub_natuple a b -> i < length a -> Ncomponent i a = Ncomponent i b. Proof. ir. assert (component i a = component i b). app component_sub_uple. uh H; ee; am. uf Ncomponent. rww H1. Qed. Lemma vertical_same_Ncomponents: forall (p q : E) (i : nat), vertical p q -> i < length p -> Ncomponent i p = Ncomponent i q. Proof. ir. assert (component i p = component i q). app vertical_same_components. uf Ncomponent. rww H1. Qed. Lemma show_verticalN: forall p q : E, natuple p -> natuple q -> length p <= length q -> (forall i : nat, i < length p -> Ncomponent i p = Ncomponent i q) -> vertical p q. Proof. ir. app show_vertical. ir. wrr R_Ncomponent. wrr R_Ncomponent. rww H2. om. Qed. Lemma Ncomponent_length_branch: forall (i : nat) (p : E), natuple p -> Ncomponent (length p) (branch i p) = i. Proof. ir. assert (component (length p) (branch i p) = R i). app component_length_branch. uf Ncomponent. rww H0. rww Bnat_R. Qed. Lemma Ncomponent_branch: forall (i j : nat) (p : E), natuple p -> i < length p -> Ncomponent i (branch j p) = Ncomponent i p. Proof. ir. assert (component i (branch j p) = component i p). app component_branch. uf Ncomponent. rww H1. Qed. Lemma Ncomponent_above: forall (i : nat) (p : E), i < length p - 1 -> Ncomponent i (above p) = Ncomponent i p. Proof. ir. assert (component i (above p) = component i p). app component_above. uf Ncomponent. rww H0. Qed. Definition horizontal p q := natuple p & natuple q & coincidence p q < length p & coincidence p q < length q & Ncomponent (coincidence p q) p < Ncomponent (coincidence p q) q. Lemma horizontal_not_vertical : forall p q, horizontal p q -> vertical p q -> False. Proof. ir. cp (vertical_common_eq H0). wri H1 H. uh H; ee. assert (coincidence (common p q) q = coincidence p q). rww H1. rwi H6 H3. rwi length_common H3. om. Qed. Lemma coincidence_symm : forall p q, Uple.axioms p -> Uple.axioms q -> coincidence p q = coincidence q p. Proof. ir. wrr length_common. rww common_symm. rww length_common. Qed. Lemma horizontal_not_vertical_inv : forall p q, horizontal p q -> vertical q p -> False. Proof. ir. cp (vertical_common_eq H0). wri H1 H. uh H; ee. assert (coincidence p (common q p) = coincidence p q). rww H1. rwi H6 H4. rwi length_common H4. assert (coincidence p q = coincidence q p). app coincidence_symm. lu. lu. om. Qed. Lemma horizontal_antisym : forall p q, horizontal p q -> horizontal q p -> False. Proof. ir. uh H; uh H0; ee. rwi coincidence_symm H4. om. lu. lu. Qed. Lemma vertical_by_coincidence : forall p q, natuple p -> natuple q -> coincidence p q = length p -> vertical p q. Proof. ir. app show_vertical. wr H1. app leq_coincidence_right. lu. lu. ir. wri H1 H2. app lt_coincidence_component_eq. lu. lu. Qed. Lemma horizontal_vertical_dichot : forall p q, natuple p -> natuple q -> (horizontal p q \/ horizontal q p \/ vertical p q \/ vertical q p). Proof. ir. cp H; cp H0; uh H; uh H0; ee. set (k:= coincidence p q). assert (k = coincidence q p). rww coincidence_symm. assert (k <= length p). uf k. app leq_coincidence_left. assert (k<= length q). uf k. app leq_coincidence_right. assert (k = length p \/ k = length q \/ (k < length p & k < length q)). om. nin H8. ap or_intror. ap or_intror. ap or_introl. app vertical_by_coincidence. nin H8. ap or_intror. ap or_intror. ap or_intror. app vertical_by_coincidence. wrr H5. ee. assert (Ncomponent k p <> Ncomponent k q). uf k. app Ncomponent_coincidence_neq. assert (Ncomponent k p < Ncomponent k q \/ Ncomponent k p > Ncomponent k q). om. nin H11. ap or_introl. uhg; ee. am. am. am. am. am. ap or_intror. ap or_introl. uhg; ee. am. am. wrr H5. wrr H5. wr H5. om. Qed. Lemma length_common_leq : forall a b k, Uple.axioms a -> Uple.axioms b -> component k a <> component k b -> length (common a b) <= k. Proof. ir. apply excluded_middle. uhg; ir. assert (k < length (common a b)). om. ap H1. transitivity (component k (common a b)). rww component_common_left. wrr length_common. rww component_common_right. wrr length_common. Qed. Lemma show_common_eq1 : forall a b c, sub_uple c a -> sub_uple c b -> length c < length a -> length c < length b -> component (length c) a <> component (length c) b -> common a b = c. Proof. ir. cp H; cp H0; uh H; uh H0; ee. assert (length (common a b) <= length c). app length_common_leq. ap sub_uple_extens. app show_sub_uple. app axioms_common. ir. rw component_common_left. assert (i < length c). om. wr H11. rww component_restrict. am. am. wrr length_common. app common_univ_sub_uple. Qed. Lemma show_common_eq : forall a b c, Uple.axioms a -> Uple.axioms b -> Uple.axioms c -> length c < length a -> length c < length b -> (forall i, i component i c = component i a) -> (forall i, i component i c = component i b) -> component (length c) a <> component (length c) b -> common a b = c. Proof. ir. ap show_common_eq1. app show_sub_uple. om. app show_sub_uple. om. am. am. am. Qed. Lemma horizontal_trans_case1 : forall p q r, horizontal p q -> horizontal q r -> length (common p q) < length (common q r) -> horizontal p r. Proof. ir. cp H; cp H0; uh H; uh H0; ee. cp H; cp H4; uh H; uh H8; uh H4; ee. wri length_common H9. wri length_common H10. wri length_common H5; wri length_common H6. assert (common p r = common p q). ap show_common_eq. am. am. app axioms_common. am. om. ir. rww component_common_left. wrr length_common. ir. transitivity (component i q). rww component_common_right. wrr length_common. transitivity (component i (common q r)). sy. app component_common_left. wr length_common. om. app component_common_right. wr length_common. om. set (k:= length (common p q)). assert (Ncomponent k p <> Ncomponent k r). assert (Ncomponent k r = Ncomponent k q). sy. ap lt_coincidence_Ncomponent_eq. am. am. wrr length_common. rw H17. wri length_common H11. uf k. om. uhg; ir. ap H17. uf Ncomponent. rww H18. uhg; ee. am. am. wr length_common. rw H17. am. wr length_common. rw H17. om. assert (coincidence p r = coincidence p q). wr length_common. wr length_common. rww H17. rw H18. set (k:= coincidence p q). assert (Ncomponent k r = Ncomponent k q). sy. ap lt_coincidence_Ncomponent_eq. am. am. wrr length_common. uf k. wrr length_common. rw H19. am. Qed. Lemma horizontal_trans_case2 : forall p q r, horizontal p q -> horizontal q r -> length (common q r) < length (common p q) -> horizontal p r. Proof. ir. cp H; cp H0; uh H; uh H0; ee. cp H; cp H4; uh H; uh H8; uh H4; ee. wri length_common H9. wri length_common H10. wri length_common H5; wri length_common H6. assert (common p r = common q r). ap show_common_eq. am. am. app axioms_common. om. am. ir. rww component_common_left. sy. app lt_coincidence_component_eq. wr length_common. om. wrr length_common. ir. rww component_common_right. wrr length_common. set (k:= length (common q r)). assert (Ncomponent k p <> Ncomponent k r). assert (Ncomponent k p = Ncomponent k q). ap lt_coincidence_Ncomponent_eq. am. am. wrr length_common. rw H17. wri length_common H7. uf k. om. uhg; ir. ap H17. uf Ncomponent. rww H18. uhg; ee. am. am. wr length_common. rw H17. om. wr length_common. rw H17. am. assert (coincidence p r = coincidence q r). wr length_common. wr length_common. rww H17. rw H18. set (k:= coincidence q r). assert (Ncomponent k p = Ncomponent k q). ap lt_coincidence_Ncomponent_eq. am. am. wrr length_common. uf k. wrr length_common. rw H19. am. Qed. Lemma horizontal_trans_case3 : forall p q r, horizontal p q -> horizontal q r -> length (common p q) = length (common q r) -> horizontal p r. Proof. ir. cp H; cp H0; uh H; uh H0; ee. cp H; cp H4; uh H; uh H8; uh H4; ee. wri length_common H9. wri length_common H10. wri length_common H5; wri length_common H6. assert (common p q = common q r). ap uple_extensionality. app axioms_common. app axioms_common. am. ir. transitivity (component i q). rww component_common_right. wrr length_common. rww component_common_left. wr length_common. wrr H1. assert (coincidence q r = coincidence p q). wrr length_common. wrr length_common. sy; am. rwi H18 H7. assert (Ncomponent (coincidence p q) p < Ncomponent (coincidence p q) r). om. assert (Ncomponent (coincidence p q) p <>Ncomponent (coincidence p q) r). om. assert (common p r = common p q). ap show_common_eq. am. am. app axioms_common. am. rww H17. ir. rww component_common_left. wrr length_common. ir. rw H17. rww component_common_right. wr length_common. wrr H17. uhg; ir. ap H20. uf Ncomponent. wr length_common. rww H21. uhg; ee. am. am. wr length_common. rw H21. am. wr length_common. rw H21. rww H1. assert (coincidence p r = coincidence p q). wr length_common. wr length_common. rww H21. rww H22. Qed. Lemma horizontal_trans : forall p r, (exists q, horizontal p q & horizontal q r) -> horizontal p r. Proof. ir. ind H q. ee. assert (length (common p q) < length (common q r) \/ length (common q r) < length (common p q) \/ length (common p q) = length (common q r)). om. nin H1. apply horizontal_trans_case1 with q. am. am. am. nin H1. apply horizontal_trans_case2 with q. am. am. am. apply horizontal_trans_case3 with q. am. am. am. Qed. Lemma horizontal_vertical_trans : forall p q, (exists r, horizontal p r & vertical r q) -> horizontal p q. Proof. ir. ind H r. ee. cp H; cp H0; uh H; uh H0; ee. cp H; cp H3; uh H; uh H3; uh H5; ee. assert (length r <= length q). app sub_uple_length_leq. assert (common p q = common p r). app show_common_eq. app axioms_common. rww length_common. rw length_common. om. ir. rww component_common_left. wrr length_common. ir. transitivity (component i r). rww component_common_right. wrr length_common. app component_sub_uple. assert (length (common p r) <= length r). app leq_length_common_right. om. rw length_common. uhg; ir. assert (Ncomponent (coincidence p r) p = Ncomponent (coincidence p r) r). transitivity (Ncomponent (coincidence p r) q). uf Ncomponent. rww H15. sy. ap Ncomponent_sub_natuple. uhg; ee. am. am. am. am. om. assert (coincidence p q = coincidence p r). wr length_common. rw H15. rww length_common. uhg; ee; try am. rww H16. rw H16. om. rw H16. assert (Ncomponent (coincidence p r) q = Ncomponent (coincidence p r) r). sy. ap Ncomponent_sub_natuple. uhg; ee. am. am. am. am. rww H17. Qed. Lemma vertical_horizontal_trans : forall p q, (exists r, vertical r p & horizontal r q) -> horizontal p q. Proof. ir. ind H r. ee. cp H; cp H0; uh H; uh H0; ee. cp H7; cp H3; uh H7; uh H3; uh H0; ee. assert (length r <= length p). app sub_uple_length_leq. assert (common p q = common q r). app show_common_eq. app axioms_common. rww length_common. rw coincidence_symm. om. am. am. rw length_common. rww coincidence_symm. ir. transitivity (component i r). rww component_common_right. wrr length_common. app component_sub_uple. assert (length (common q r) <= length r). app leq_length_common_right. om. rw length_common. ir. rww component_common_left. uhg; ir. assert (Ncomponent (coincidence r q) q = Ncomponent (coincidence r q) r). transitivity (Ncomponent (coincidence r q) p). uf Ncomponent. rww coincidence_symm. wr length_common. rww H15. sy. ap Ncomponent_sub_natuple. uhg; ee. am. am. am. am. om. assert (coincidence p q = coincidence r q). wr length_common. rw H15. rww length_common. app coincidence_symm. uhg; ee; try am. rww H16. om. rww H16. assert (Ncomponent (coincidence r q) p = Ncomponent (coincidence r q) r). sy. ap Ncomponent_sub_natuple. uhg; ee. am. am. am. am. rw H16. rww H17. Qed. Definition natuples_of_length k := Z (Function_Set.function_set k (fun x => nat)) natuple. Lemma inc_natuples_of_length : forall a k, inc a (natuples_of_length k) = (natuple a & R (length a) = k). Proof. ir. ap iff_eq; ir. ufi natuples_of_length H. Ztac. cp (Function_Set.function_set_pr H0). ee. uf length. rw R_Bnat. am. uh H1; ee. uh H1; ee. am. ee. uf natuples_of_length. ap Z_inc. uh H; ee. uh H; ee. app Function_Set.function_set_inc. ufi length H0. rwi R_Bnat H0. am. am. ir. set (j:= Bnat y). assert (R j = y). uf j. rw R_Bnat. tv. ap inc_nat_from_inc_R. sh (length a). rww H0. assert (V y a = component j a). uf component. rww H4. rw H5. ap H1. wr inc_lt. rw H0. rww H4. am. Qed. Definition natuples_substrate := Image.create nat (fun k => natuples_of_length k). Lemma inc_natuples_substrate : forall x, inc x natuples_substrate = (exists k, inc k nat & natuples_of_length k = x). Proof. ir. ap iff_eq; ir. ufi natuples_substrate H. rwi Image.inc_rw H. am. uf natuples_substrate. rw Image.inc_rw. am. Qed. Definition natuples := union natuples_substrate. Lemma inc_natuples : forall a, inc a natuples = natuple a. Proof. ir. ap iff_eq; ir. ufi natuples H. cp (union_exists H). ind H0 y. ee. rwi inc_natuples_substrate H1. ind H1 k. ee. wri H2 H0. rwi inc_natuples_of_length H0. ee. am. uf natuples. apply union_inc with (natuples_of_length (R (length a))). rw inc_natuples_of_length. ee. am. tv. rw inc_natuples_substrate. sh (R (length a)). ee. ap R_inc. tv. Qed. End TreeIndex. Module Tree. Export TreeIndex. Export Cardinal. Lemma sub_natuples_rw : forall t, sub t natuples = (forall v, inc v t -> natuple v). Proof. ir. ap iff_eq; ir. wr inc_natuples. app H. uhg; ir. rw inc_natuples; au. Qed. Definition above_closed t := sub t natuples & (forall v, inc v t -> inc (above v) t). Definition branch_left_closed t := sub t natuples & (forall v i j, inc v t -> inc (branch j v) t -> i < j -> inc (branch i v) t). Definition is_tree t := is_finite t & sub t natuples & nonempty t & (forall v, inc v t -> inc (above v) t) & (forall v i j, inc v t -> inc (branch j v) t -> i < j -> inc (branch i v) t). Lemma is_tree_rw : forall t, is_tree t = (is_finite t & nonempty t & above_closed t & branch_left_closed t). Proof. ir. ap iff_eq; ir. uh H; ee. am. am. uhg; ee. am. am. uhg; ee; am. uhg; ee. am. uh H1; ee; am. am. uh H1; ee; am. uh H2; ee. am. Qed. Lemma tree_branch_left_closed : forall t, is_tree t -> branch_left_closed t. Proof. ir. rwi is_tree_rw H. ee; am. Qed. Lemma inc_tree_natuple : forall v, (exists t, is_tree t & inc v t) -> natuple v. Proof. ir. ind H t. ee. uh H; ee. assert (inc v natuples). ap H1. am. rwi inc_natuples H5. am. Qed. Lemma tree_finite : forall t, is_tree t -> is_finite t. Proof. ir. uh H; ee; am. Qed. Lemma tree_nonempty : forall t, is_tree t -> nonempty t. Proof. ir. uh H; ee; am. Qed. Lemma tree_above_closed : forall t, is_tree t -> above_closed t. Proof. ir. rwi is_tree_rw H. ee; am. Qed. Definition branch_index v := Ncomponent (length v - 1) v. Lemma R_branch_index : forall v, nonroot v -> R (branch_index v) = last_component v. Proof. ir. uf branch_index. rw R_Ncomponent. uf last_component. tv. uh H; ee. am. uh H; ee. om. Qed. Lemma branch_branch_index_above : forall v, nonroot v -> branch (branch_index v) (above v) = v. Proof. ir. uf branch. rw R_branch_index. rw utack_last_component. tv. am. am. Qed. Lemma branch_index_branch : forall i v, natuple v -> branch_index (branch i v) = i. Proof. ir. uf branch_index. rw length_branch. assert (length v + 1 - 1 = length v). om. rw H0. rww Ncomponent_length_branch. am. Qed. Definition below v w := natuple v & (exists i, branch i v = w). Lemma below_above_eq : forall v w, below v w -> above w = v. Proof. ir. uh H; ee. ind H0 i. wr H0. rww above_branch. Qed. Lemma below_nonroot : forall v w, below v w -> nonroot w. Proof. ir. uh H; ee. ind H0 i. wr H0. app nonroot_branch. Qed. Lemma below_rw : forall v w, below v w = (natuple v & natuple w & branch (branch_index w) v = w). Proof. ir. ap iff_eq; ir. ee. uh H; ee. am. uh H; ee. ind H0 i. wr H0. app natuple_branch. cp (below_above_eq H). wr H0. rw branch_branch_index_above. tv. apply below_nonroot with v. am. ee. uhg; ee. am. sh (branch_index w). am. Qed. Lemma below_vertical : forall v w, below v w -> vertical v w. Proof. ir. cp (below_above_eq H). wr H0. ap vertical_above. rwi below_rw H. ee; am. Qed. Lemma nonroot_below_above : forall v, nonroot v -> below (above v) v. Proof. ir. cp (branch_branch_index_above H). uhg; ee. ap natuple_above. uh H; ee; am. sh (branch_index v). am. Qed. Lemma vertical_below : forall v w, vertical v w -> length w = length v + 1 -> below v w. Proof. ir. assert (above w = v). ap natuple_extensionality. ap natuple_above. uh H; ee; am. uh H; ee; am. rw length_above. om. uh H; ee; am. ir. rw Ncomponent_above. sy. ap vertical_same_Ncomponents. am. rwi length_above H1. om. uh H; ee; am. rwi length_above H1. om. uh H; ee; am. wr H1. ap nonroot_below_above. uhg; ee. uh H; ee; am. om. Qed. Lemma below_branch : forall v i, natuple v -> below v (branch i v). Proof. ir. uhg; ee. am. sh i. tv. Qed. Definition branches t v := Z t (below v). Lemma inc_branches_rw : forall t v w, inc w (branches t v) = (inc w t & below v w). Proof. ir. uf branches. ap iff_eq; ir. Ztac. ee. Ztac. Qed. Lemma sub_branches_t : forall t v, sub (branches t v) t. Proof. ir. uhg; ir. rwi inc_branches_rw H. ee; am. Qed. Lemma inc_branches_nonroot : forall t v w, inc w (branches t v) -> nonroot w. Proof. ir. rwi inc_branches_rw H. ee. apply below_nonroot with v. am. Qed. Definition branch_coords t v := Image.create (branches t v) last_component. Lemma inc_branch_coords_rw : forall t v k, natuple v -> inc k (branch_coords t v) = (exists i, R i = k & inc (branch i v) t). Proof. ir. assert (lemA : natuple v). am. clear H. ap iff_eq; ir. ufi branch_coords H. rwi Image.inc_rw H. ind H z. ee. rwi inc_branches_rw H. ee. sh (Bnat k). ee. uh H1. ee. uh H1; ee. rw R_Bnat. tv. ind H2 i. wri H2 H0. rwi last_component_branch H0. wr H0. app R_inc. uhg; ee. am. am. uh H1; ee. cp H1; uh H1; ee. ind H2 i. wri H2 H0. rwi last_component_branch H0. wr H0. rw Bnat_R. rw H2. am. am. ind H i. ee. uf branch_coords. rw Image.inc_rw. sh (branch i v). ee. rw inc_branches_rw. ee. am. app below_branch. rw last_component_branch. tv. am. Qed. Lemma inc_branch_coords_rw2 : forall t v k, natuple v -> inc k (branch_coords t v) = (inc k nat & inc (branch (Bnat k) v) t). Proof. ir. rww inc_branch_coords_rw. ap iff_eq; ir. ind H0 i. ee. wr H0. ap R_inc. wr H0. rw Bnat_R. am. sh (Bnat k). ee. rww R_Bnat. am. Qed. Lemma inc_R_branch_coords : forall t v (i:nat), natuple v -> inc (R i) (branch_coords t v) = inc (branch i v) t. Proof. ir. rww inc_branch_coords_rw. ap iff_eq; ir. ind H0 j. ee. assert (j= i). app R_inj. wrr H2. sh i. ee. tv. am. Qed. Lemma sub_branch_coords_nat : forall t v, natuple v -> sub (branch_coords t v) nat. Proof. ir. uhg; ir. rwi inc_branch_coords_rw2 H0. ee; am. am. Qed. Lemma is_finite_branches : forall t v, is_finite t -> is_finite (branches t v). Proof. ir. ap Infinite.subset_finite. sh t. ee. ap sub_branches_t. am. Qed. Lemma is_finite_branch_coords : forall t v, is_finite t -> is_finite (branch_coords t v). Proof. ir. uf branch_coords. ap Infinite.image_finite. app is_finite_branches. Qed. Definition lower_saturated_nat_subset x := sub x nat & (forall i j, i < j -> inc (R j) x -> inc (R i) x). Lemma lsns_ordinal : forall x, lower_saturated_nat_subset x -> is_ordinal x. Proof. ir. uh H; ee. ap Infinite.ordinal_criterion. ir. assert (inc x0 nat). app H. apply ordinal_inc_ordinal with nat. ap Infinite.is_ordinal_nat. am. ir. assert (ordinal_lt y nat). ap Infinite.ordinal_lt_trans. sh x0. ee. am. rw ordinal_lt_rw. ee. ap Infinite.is_ordinal_nat. au. rwi ordinal_lt_rw H2; rwi ordinal_lt_rw H3; ee. assert (R (Bnat y) = y). rww R_Bnat. wr H6. apply H0 with (Bnat x0). wr inc_lt. rww R_Bnat. rww R_Bnat. au. rww R_Bnat. au. Qed. Lemma lsns_or : forall x, lower_saturated_nat_subset x -> (inc x nat \/ x = nat). Proof. ir. assert (is_ordinal x). app lsns_ordinal. assert (is_ordinal nat). ap Infinite.is_ordinal_nat. cp (ordinal_lt_lt_eq_or H0 H1). nin H2. ap or_introl. rwi ordinal_lt_rw H2; ee; am. nin H2. assert (ordinal_leq x nat). uhg. ee. am. am. uh H; ee; am. cp (Infinite.ordinal_not_leq_lt H3 H2). elim H4. app or_intror. Qed. Lemma lsns_inc_nat : forall x, lower_saturated_nat_subset x -> is_finite x -> inc x nat. Proof. ir. cp (lsns_or H). nin H1. am. rwi H1 H0. cp (Infinite.is_infinite_nat). uh H2; ee. cp (H2 H0). elim H3. Qed. Lemma lsns_branch_coords : forall t v, branch_left_closed t -> inc v t -> lower_saturated_nat_subset (branch_coords t v). Proof. ir. assert (natuple v). wr inc_natuples. uh H; ee; au. uhg. ee. app sub_branch_coords_nat. ir. rwi inc_R_branch_coords H3. rww inc_R_branch_coords. uh H; ee. apply H4 with j. am. am. am. am. Qed. Lemma inc_branch_coords_nat_blc : forall t v, branch_left_closed t -> inc v t -> is_finite t -> inc (branch_coords t v) nat. Proof. ir. ap lsns_inc_nat. app lsns_branch_coords. ap is_finite_branch_coords. am. Qed. Lemma inc_branch_coords_nat : forall t v, is_tree t -> inc v t -> inc (branch_coords t v) nat. Proof. ir. uh H; ee. app inc_branch_coords_nat_blc. uhg; ee. am. am. Qed. Definition vertex_arity t v := Bnat (branch_coords t v). Lemma R_vertex_arity_blc : forall t v, branch_left_closed t -> is_finite t -> inc v t -> R (vertex_arity t v) = branch_coords t v. Proof. ir. uf vertex_arity. rw R_Bnat. tv. app inc_branch_coords_nat_blc. Qed. Lemma R_vertex_arity : forall t v, is_tree t -> inc v t -> R (vertex_arity t v) = branch_coords t v. Proof. ir. ap R_vertex_arity_blc. app tree_branch_left_closed. uh H; ee; am. am. Qed. Lemma inc_branch_lt_vertex_arity_blc : forall t v i, is_finite t -> branch_left_closed t -> inc v t -> (inc (branch i v) t) = (i < vertex_arity t v). Proof. ir. assert (natuple v). wr inc_natuples. uh H0; ee. au. ap iff_eq; ir. wr inc_lt. rw R_vertex_arity_blc. rw inc_R_branch_coords. am. am. am. am. am. wri inc_lt H3. rwi R_vertex_arity_blc H3. rwi inc_R_branch_coords H3. am. am. am. am. am. Qed. Lemma inc_branch_lt_vertex_arity : forall t v i, is_tree t -> inc v t -> (inc (branch i v) t) = (i < vertex_arity t v). Proof. ir. ap inc_branch_lt_vertex_arity_blc. uh H; ee; am. app tree_branch_left_closed. am. Qed. Definition is_end t v := is_tree t & inc v t & (forall w, inc w t -> vertical v w -> w = v). Lemma sub_uple_restrict : forall u k, Uple.axioms u -> k <= length u -> sub_uple (restrict u k) u. Proof. ir. uhg; ee. app restrict_axioms. am. rww length_restrict. rww length_restrict. Qed. Lemma restrict_restrict : forall u i j, i<= j -> j <= length u -> restrict (restrict u j) i = restrict u i. Proof. ir. ap uple_extensionality. app restrict_axioms. app restrict_axioms. rww length_restrict. rww length_restrict. ir. rwi length_restrict H1. rww component_restrict. rww component_restrict. rww component_restrict. om. Qed. Lemma sub_uple_of_restrict : forall u v k, sub_uple u v -> k <= length v -> length u <= k -> sub_uple u (restrict v k). Proof. ir. uhg; ee. uh H; ee; am. ap restrict_axioms. rww length_restrict. rww restrict_restrict. uh H; ee. am. Qed. Lemma natuple_restrict : forall u k, natuple u -> k <= length u -> natuple (restrict u k). Proof. ir. uhg; ee. app restrict_axioms. ir. rww component_restrict. rwi length_restrict H1. uh H; ee. ap H2. om. rwi length_restrict H1. am. Qed. Lemma vertical_restrict : forall u k, natuple u -> k <= length u -> vertical (restrict u k) u. Proof. ir. uhg; ee. app natuple_restrict. am. app sub_uple_restrict. uh H; ee; am. Qed. Lemma vertical_of_restrict : forall u v k, vertical u v -> k <= length v -> length u <= k -> vertical u (restrict v k). Proof. ir. uhg; ee. uh H; ee; am. app natuple_restrict. uh H; ee; am. ap sub_uple_of_restrict. uh H; ee; am. am. am. Qed. Lemma above_restrict : forall u k, k<= length u -> above (restrict u k) = restrict u (k-1). Proof. ir. uf above. rw length_restrict. rw restrict_restrict. tv. om. am. Qed. Lemma above_closed_vertical_closed : forall t u, above_closed t -> (exists v, (inc v t & vertical u v)) -> inc u t. Proof. ir. ind H0 v. ee. assert (forall i, inc (restrict v (length v -i)) t). ir. nin i. assert (length v - 0 = length v). om. rw H2. rw restrict_full_length. am. uh H1; ee. uh H3; ee; am. assert (length v - (S i) = (length v - i) -1). om. rw H2. wr above_restrict. uh H; ee. ap H3. am. om. uh H1; ee. uh H4; ee. assert (length u = (length v - (length v - length u))). om. rwi H8 H7. wr H7. ap H2. Qed. Lemma tree_vertical_closed : forall t u, is_tree t -> (exists v, (inc v t & vertical u v)) -> inc u t. Proof. ir. app above_closed_vertical_closed. app tree_above_closed. Qed. Lemma inc_emptyset_tree : forall t, is_tree t -> inc emptyset t. Proof. ir. ap tree_vertical_closed. am. uh H; ee. nin H1. sh y. ee. am. ap vertical_emptyset. wr inc_natuples. app H0. Qed. Lemma cardinality_branches : forall t v, is_tree t -> inc v t -> cardinality (branches t v) = R (vertex_arity t v). Proof. ir. uf vertex_arity. rw R_Bnat. transitivity (cardinality (branch_coords t v)). ap cardinality_invariant. rw Map.iso_trans_ex_rw. sh last_component. uf branch_coords. apply Transformation.trans_sub_bijective with (x:= branches t v) (y:= nat). uhg; ee. uhg. ir. rwi inc_branches_rw H1. ee. assert (natuple x). wr inc_natuples. uh H; ee; au. uh H3; ee. uf last_component. ap H4. assert (length x > 0). uh H2; ee. ind H5 i. wr H5. uf branch. rw length_utack. om. uh H2; ee; am. om. uhg; ir. rwi inc_branches_rw H1; rwi inc_branches_rw H2. ee. uh H4; uh H5; ee. ind H7 i. ind H6 j. wri H7 H3. wri H6 H3. rwi last_component_branch H3. rwi last_component_branch H3. assert (i=j). app R_inj. wr H7. rww H8. am. am. uhg; ir; am. ap Infinite.nat_cardinality_refl. app inc_branch_coords_nat. app inc_branch_coords_nat. Qed. Lemma is_end_arity_zero : forall t v, is_tree t -> inc v t -> is_end t v = (vertex_arity t v = 0). Proof. ir. assert (natuple v). wr inc_natuples. uh H; ee; au. ap iff_eq; ir. uh H2. ee. assert (~(0 < vertex_arity t v)). uhg; ir. wri inc_branch_lt_vertex_arity H5. assert (vertical v (branch 0 v)). app vertical_branch. cp (H4 _ H5 H6). assert (length (branch 0 v) = length v). rww H7. rwi length_branch H8. om. am. am. am. om. uhg; ee. am. am. ir. assert (length v = length w). assert (length v <= length w). uh H4; ee. uh H6; ee. am. assert (~(length v < length w)). uhg; ir. set (u:= restrict w (length v + 1)). assert (vertical u w). uf u. ap vertical_restrict. uh H4; ee; am. om. assert (vertical v u). uf u. ap vertical_of_restrict. am. om. om. assert (below v u). app vertical_below. uf u. rww length_restrict. assert (inc u (branches t v)). rw inc_branches_rw. ee. uh H; ee. ap tree_vertical_closed. uhg; ee; am. sh w. ee. am. am. am. assert (cardinality (branches t v) = R 0). rw cardinality_branches. rww H2. am. am. cp (Infinite.cardinality_zero_empty H11). rwi H12 H10. nin H10. nin x. om. uh H4; ee. uh H7; ee. wr H10. rw H5. rww restrict_full_length. Qed. End Tree.