proposition: Lemma exists_CompletelyUnConstrFreshIdx: forall (qs_schema : RawQueryStructureSchema) (BagIndexKeys : ilist3 (qschemaSchemas qs_schema)) (r_o : UnConstrQueryStructure qs_schema) (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> exists bnd : nat, forall idx : Fin.t (numRawQSschemaSchemas qs_schema), UnConstrFreshIdx (GetUnConstrRelation r_o idx) bnd.
proof: Proof. intros. generalize (exists_UnConstrFreshIdx H); clear H. remember (GetUnConstrRelation r_o); clear. destruct qs_schema; simpl in *. clear qschemaConstraints. induction numRawQSschemaSchemas; simpl in *; intros. - exists 0; intros; inversion idx. - revert i IHnumRawQSschemaSchemas H. pattern numRawQSschemaSchemas, qschemaSchemas; apply Vector.caseS; simpl; intros. destruct (IHnumRawQSschemaSchemas t (fun idx => i (Fin.FS idx)) (fun idx => H (Fin.FS idx)) ). destruct (H Fin.F1). exists (max x x0). unfold UnConstrFreshIdx in *; simpl in *; intros. pose proof (Max.le_max_l x x0); pose proof (Max.le_max_r x x0). generalize dependent idx; intro; generalize t i x x0 H0 H1 H3 H4; clear; pattern n, idx; apply Fin.caseS; simpl; intros. apply H1 in H2; omega. apply H0 in H2; omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.Examples.HACMSDemo.DuplicateFree Fiat.QueryStructure.Automation.MasterPlan Bedrock.Word Bedrock.Memory