fact: Definition QSMutateSpec (qs_schema : QueryStructureSchema) (qs : QueryStructure qs_schema) (Ridx : _) (MutatedTuples : @IndexedEnsemble (@RawTuple (GetNRelSchemaHeading _ Ridx))) (qs' : QueryStructure qs_schema) : Prop := (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx)) /\ (MutationPreservesTupleConstraints MutatedTuples (SatisfiesTupleConstraints Ridx)) /\ (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetRelation qs' Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx')) /\ (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (GetRelation qs' Ridx') MutatedTuples (SatisfiesCrossRelationConstraints Ridx' Ridx)) /\ (Same_set _ (GetRelation qs' Ridx) MutatedTuples) /\ (forall Ridx', Ridx <> Ridx' -> Same_set _ (GetRelation qs Ridx') (GetRelation qs' Ridx')) \/ ((~ MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx) \/ (~ MutationPreservesTupleConstraints MutatedTuples (SatisfiesTupleConstraints Ridx)) \/ ~ (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetRelation qs Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx')) \/ ~ (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (GetRelation qs Ridx') MutatedTuples (SatisfiesCrossRelationConstraints Ridx' Ridx))) /\ (forall r, Same_set _ (GetRelation qs' r) (GetRelation qs r))).
imports: Coq.Lists.List Coq.Strings.String Coq.Sets.Ensembles Coq.Arith.Arith Fiat.Computation.Core Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.Common.ilist Fiat.Common.StringBound Fiat.Common.Ensembles.IndexedEnsembles Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure