h&      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                      Safe-Inferred Safe-Inferred twee-lib An array.twee-libThe contents of the array.twee-lib!A type which has a default value.twee-libThe default value.twee-lib3Convert an array to a list of (index, value) pairs.twee-libCreate an empty array.twee-lib!Create an array with one element.twee-libIndex into an array. O(1) time.twee-libIndex into an array. O(1) time.twee-libUpdate the array. O(n) time. Safe-Inferred! twee-libA heap.twee-libTake the union of two heaps.twee-libA singleton heap.twee-libThe empty heap.twee-libInsert an element.twee-lib$Find and remove the minimum element.twee-lib;Get the elements of a heap as a list, in unspecified order.twee-lib>Map a function over a heap, removing all values which map to . May be more efficient when the function being mapped is mostly monotonic.twee-lib*Return the number of elements in the heap.  Safe-Inferred%&Ktwee-libA value of type a" which has been given a unique ID.Ltwee-libThe unique ID of a label.Mtwee-lib Construct a K a' from its unique ID, which must be the L of an already existing K. Extremely unsafe!Ntwee-libAssign a label to a value.Otwee-lib*Recover the underlying value from a label.KLMNOKMLNO Safe-Inferred twee-libAn array of key-value pairs.twee-libAn empty array.twee-libA singleton array.twee-libConvert a list of pairs to an array. Duplicate keys are allowed.twee-libConvert an array to a list.twee-lib9Get the number of key-value pairs in an array. O(1) time.twee-lib Index into the array. O(1) time.twee-libLook up the value associated with a particular key. If the key occurs multiple times, any of its values may be returned. O(n) time.twee-libAssociate a value with a key. Any existing occurences of the key are removed. O(n) time.twee-libRemove a given key. O(n) time.twee-libModify the value associated with a given key. If the key occurs multiple times, one of its values is chosen and the others deleted. In the call modify k def f , if the key k is not present, the entry  k -> f def is added. O(n) time.twee-lib&Keep only keys satisfying a predicate.  Safe-Inferred_twee-lib'A sequence, stored in a serialised formtwee-libAn empty sequence.twee-libIs a given sequency empty?twee-lib'Find the number of items in a sequence.twee-libConvert a list into a sequence.twee-libConvert a sequence into a list.twee-lib0Find and remove the first value from a sequence. Safe-Inferred %&!twee-lib'A "standard" type of batches. By using Queue (StandardBatch a)0, you will get a queue where entries have type a and labels have type ().twee-lib3The type of batches must be a member of this class.twee-libEach batch can have an associated label, which is specified when calling . A label represents a piece of information which is shared in common between all entries in a batch, and which might be used to store that batch more efficiently. Labels are optional, and by default  Label a = ().twee-lib Individual entries in the batch.twee-libGiven a label, and a non-empty list of entries, sorted in ascending order, produce a list of batches.twee-lib'Remove the smallest entry from a batch.twee-libReturn the label of a batch.twee-lib%Compute the size of a batch. Used in ;. The default implementation works by repeatedly calling .twee-libA queue of batches.twee-lib'Convert a batch into a list of entries.twee-libThe empty queue.twee-libAdd entries to the queue.twee-lib(Remove the minimum entry from the queue.twee-libRemove the minimum entry from the queue, discarding any batches that do not satisfy the predicate.twee-libMap a function over all entries. The function must preserve the label of each batch, and must not split existing batches into two.twee-lib=Convert a queue into a list of batches, in unspecified order.twee-lib=Convert a queue into a list of entries, in unspecified order. Safe-Inferred"%&"1STUVSTUV Safe-Inferred%&#Wtwee-libA task which runs in the monad m and produces a value of type a.Xtwee-libCreate a new task that should be run a certain proportion of the time. The first argument is how often in seconds the task should run, at most. The second argument is the maximum percentage of time that should be spent on the task.Ytwee-lib"Run a task if it's time to run it.WXYWXY Safe-Inferred "%&(+Ztwee-libA monoid for building terms. & represents the empty termlist, while  appends two termlists.[twee-lib A variable.]twee-libThe variable's number. Don't use huge variable numbers: they will be truncated to 32 bits when stored in a term.^twee-libA function symbol. f is the underlying type of function symbols defined by the user; ^ f is an f8 together with an automatically-generated unique number._twee-libThe unique number of a ^. Must fit in 32 bits.`twee-lib` f, is a term whose function symbols have type f. It is either a [ or an b.atwee-liba f5 is a list of terms whose function symbols have type f. It is either a m or an n. You can turn it into a [` f] with .btwee-libMatches a function application.ctwee-libMatches a variable.dtwee-libLike h, but does not check that the termlist is non-empty. Use only if you are sure the termlist is non-empty.htwee-lib:Matches a non-empty termlist, unpacking it into head and -everything except the root symbol of the head;. Useful for iterating through terms one symbol at a time.For example, if ts is the termlist [f(x,y), g(z)], then let ConsSym u us = ts# results in the following bindings: u = f(x,y) us = [x, y, g(z)]ltwee-libLike m, but does not check that the termlist is non-empty. Use only if you are sure the termlist is non-empty.mtwee-lib>Matches a non-empty termlist, unpacking it into head and tail.ntwee-libMatches the empty termlist.otwee-libIndex into a termlist.twee-lib/Index into a termlist, without bounds checking.ptwee-lib0The length of (number of symbols in) a termlist.qtwee-libConvert a term to a termlist.rtwee-lib5Is a term contained as a subterm in a given termlist?twee-lib)Check if a variable occurs in a termlist.=Z[]\^_`abcdefghijklmnopqr Safe-Inferred,}stuvwxyz{|}~yz{|}~wxuvst Safe-Inferred "(<Dtwee-libA triangle substitution is one in which variables can be defined in terms of each other, though not in a circular way.:The main use of triangle substitutions is in unification;  returns one. A triangle substitution can be converted to an ordinary substitution with , or used directly using its  instance.twee-lib5A substitution which maps variables to terms of type ` f.twee-lib.A class for values which act as substitutions.Instances include . as well as functions from variables to terms.twee-lib(The underlying type of function symbols.twee-lib%Apply the substitution to a variable.twee-lib%Apply the substitution to a termlist.twee-lib Instances of  can be turned into terms using  or ', and turned into term builders using . Has instances for terms, termlists, builders, and Haskell lists.twee-lib(The underlying type of function symbols.twee-libConvert a value into a Z.twee-libA pattern which extracts the  from a ^.twee-lib>Build a term. The given builder must produce exactly one term.twee-libBuild a termlist.twee-lib0Build a constant (a function with no arguments).twee-libBuild a function application.twee-libBuild a variable.twee-lib-Convert a substitution to a list of bindings.twee-lib$Fold a function over a substitution.twee-libCheck if all bindings of a substitution satisfy a given property.twee-lib5Compute the set of variables bound by a substitution.twee-libApply a substitution to a term.twee-lib=D@ACBIEFHGJ  !"#$%&'()*+,-./0123456789:;?<>=D@ACBIEFHGJ6 Safe-Inferred%&Omtwee-lib7Describes whether an inequality is strict or nonstrict.twee-lib0The first term is strictly less than the second.twee-lib3The first term is less than or equal to the second.twee-libReturn  if the first term is less than or equal to the second, in the term ordering.twee-libCheck if the first term is less than or equal to the second in the given model, and decide whether the inequality is strict or nonstrict.twee-libReturn  if the first argument is strictly less than the second, in the term ordering.twee-libReturn the direction in which the terms are oriented according to the term ordering, or ) if they cannot be oriented. A result of  ) means that the first term is less than  or equal to the second.33 Safe-Inferred%&/8<[Jtwee-lib&A hack for encoding Horn clauses. See !. The default implementation of  should work OK.twee-libFor types which have a notion of size. | The collection of constraints which the type of function symbols must satisfy in order to be used by twee.twee-lib An instance  a b indicates that a value of type a contains a value of type b- which is somehow part of the meaning of the a.A number of functions use  constraints to work in a more general setting. For example, the functions in 4 operate on rewrite rules, but actually accept any a satisfying  a (  f).Use taste when definining $ instances; don't do it willy-nilly.twee-libGet at the thing.twee-lib3The underlying type of function symbols of a given .twee-lib"A builder compatible with a given .twee-lib0A triangle substitution compatible with a given .twee-lib'A substitution compatible with a given .twee-lib#A termlist compatible with a given .twee-libA term compatible with a given .twee-libGeneralisation of term functionality to things that contain terms (e.g., rewrite rules and equations).twee-lib Compute a  of all terms which appear in the argument (used for e.g. computing free variables). See also .twee-lib&Apply a substitution. When using the  type class, you can use  instead.twee-lib2Represents a unique identifier (e.g., for a rule).twee-libApply a substitution.twee-lib(Find all terms occuring in the argument.twee-lib-Find the variables occurring in the argument.twee-libTest if the argument is ground.twee-lib4Find the function symbols occurring in the argument.twee-lib>Count how many times a function symbol occurs in the argument.twee-lib7Count how many times a variable occurs in the argument.twee-libRename the argument so that variables are introduced in a canonical order (starting with V0, then V1 and so on).twee-libRename the second argument so that it does not mention any variable which occurs in the first.twee-lib>Return an x such that no variable >= x occurs in the argument.twee-lib(Check if a term is the minimal constant.twee-lib%Build the minimal constant as a term.twee-libErase a given set of variables from the argument, replacing them with the minimal constant.twee-libErase all except a given set of variables from the argument, replacing them with the minimal constant.twee-libReplace all variables in the argument with the minimal constant.  !"#$%&'()*+,-./0123456789:;?<>=D@ACBIEFHGJZ[\]^_`abcdefghijklmnopqrZ[\]^_`abcdefghijklmnopqr  Safe-Inferred "%&a twee-libA term index: a multimap from ` f to a.twee-lib8Check the invariant of an index. For debugging purposes.twee-libAn empty index.twee-libIs the index empty?twee-libAn index with one entry.twee-libInsert an entry into the index.twee-libDelete an entry from the index.twee-libLook up a term in the index. Finds all key-value such that the search term is an instance of the key, and returns an instance of the the value which makes the search term exactly equal to the key.twee-lib"Look up a term in the index. Like , but returns the exact value that was inserted into the index, not an instance. Also returns a substitution which when applied to the value gives you the matching instance.twee-lib!Return all elements of the index.twee-lib$Create an index from a list of itemstwee-lib$Create an index from a list of items    Safe-Inferredctwee-libOrder an equation roughly left-to-right, and canonicalise its variables. There is no guarantee that the result is oriented.twee-lib.Apply a function to both sides of an equation.twee-lib!Is an equation of the form t = t?twee-libA total order on equations. Equations with lesser terms are smaller.twee-lib#Match one equation against another.    Safe-Inferred "%&o&twee-lib6A proof, with all axioms and lemmas explicitly listed.twee-libThe used axioms.twee-libThe used lemmas.twee-libThe goals proved.twee-libOptions for proof presentation.twee-libNever inline lemmas.twee-libInline all lemmas.twee-libMake the proof ground.twee-lib!Print out explicit substitutions.twee-libPrint out proofs in colour.twee-lib3Print out which instances of some axioms were used.twee-libThe number of the axiom. Has no semantic meaning; for convenience only.twee-libA description of the axiom. Has no semantic meaning; for convenience only.twee-lib%The equation which the axiom asserts.twee-libA derivation is an unchecked proof. It might be wrong! The way to check it is to call  to turn it into a .twee-lib:Apply an existing rule (with proof!) to the root of a termtwee-lib$Apply an axiom to the root of a termtwee-lib Reflexivity.  t proves t = t.twee-libSymmetrytwee-lib Transivititytwee-libCongruence. Parallel, i.e., takes a function symbol and one derivation for each argument of that function.twee-lib-A checked proof. If you have a value of type Proof f0, it should jolly well represent a valid proof!The only way to construct a Proof f is by using .twee-lib Checks a - and, if it is correct, returns a certified .If the # is incorrect, throws an exception.twee-libSimplify a derivation so that: * Symm occurs innermost * Trans is right-associated * Each Cong has at least one non-Refl argument * Refl is not used unnecessarilytwee-libTransform a derivation into a list of single steps. Each step has the following form: * Trans does not occur * Symm only occurs innermost, i.e., next to UseLemma or UseAxiom * Each Cong has exactly one non-Refl argument (no parallel rewriting) * Refl only occurs as an argument to Congtwee-libConvert a list of steps (plus the equation it is proving) back to a derivation.twee-lib/Find all lemmas which are used in a derivation.twee-libFind all lemmas which are used in a derivation, together with the substitutions used.twee-lib/Find all axioms which are used in a derivation.twee-libFind all axioms which are used in a derivation, together with the substitutions used.twee-libFind all ground instances of axioms which are used in the expanded form of a derivation (no lemmas).twee-lib4Applies a derivation at a particular path in a term.twee-libThe default configuration.twee-lib Construct a  ProvedGoal.twee-lib5Check that pg_goal/pg_witness match up with pg_proof.twee-libSimplify and present a proof.twee-libPrint a presented proof.twee-libFormat an equation nicely.$Used both here and in the main file.;;  Safe-Inferred"%&}$twee-libA reduction proof is just a sequence of rewrite steps, stored as a list in reverse order. In each rewrite step, all subterms that are exactly equal to the LHS of the rule are replaced by the RHS, i.e. the rewrite step is performed as a parallel rewrite without matching.twee-lib9A strategy gives a set of possible reductions for a term.twee-libA rule's orientation. and % rules are used only left-to-right.  and  rules are used bidirectionally.twee-libAn oriented rule.twee-libA weakly oriented rule. The first argument is the minimal constant, the second argument is a list of terms which are weakly oriented in the rule.A rule with orientation  k ts" can be used unless all terms in ts are equal to k.twee-libA permutative rule.A rule with orientation  ts can be used if  map fst ts# is lexicographically greater than  map snd ts.twee-libAn unoriented rule.twee-libA rewrite rule.twee-lib7Information about whether and how the rule is oriented.twee-libA proof that the rule holds.twee-libThe left-hand side of the rule.twee-lib The right-hand side of the rule.twee-lib&Is a rule oriented or weakly oriented?twee-libTurn a rule into an equation.twee-libTurn an equation t :=: u into a rule t -> u by computing the orientation info (e.g. oriented, permutative or unoriented).Crashes if either t < u, or there is a variable in u which is not in t&. To avoid this problem, combine with .twee-lib6Flip an unoriented rule so that it goes right-to-left.twee-lib:Compute the normal form of a term wrt only oriented rules.twee-libCompute the normal form of a term wrt only oriented rules, using outermost reduction.twee-libCompute the normal form of a term wrt only oriented rules, using innermost reduction.twee-lib2Find a simplification step that applies to a term.twee-lib%Transitivity for reduction sequences.twee-libCompute the final term resulting from a reduction, given the starting term.twee-libTurn a reduction into a proof.twee-lib+Normalise a term wrt a particular strategy.twee-libCompute all normal forms of a set of terms wrt a particular strategy.twee-libCompute all successors of a set of terms (a successor of a term t is a term u such that t ->* u).twee-lib$Apply a strategy anywhere in a term.twee-libApply a strategy anywhere in a term, preferring outermost reductions.twee-libApply a strategy anywhere in a term, preferring innermost reductions.twee-lib)A strategy which rewrites using an index.twee-lib'A strategy which applies one rule only.twee-lib>Check if a rule can be applied, given an ordering <= on terms.twee-lib(Check if a rule can be applied normally.twee-lib/Check if a rule can be applied and is oriented.twee-lib5Check if a rule can be applied in a particular model.twee-libCheck if a rule can be applied to the Skolemised version of a term.**  Safe-Inferred %&~   Safe-Inferredtwee-libCompute the size.twee-lib.Check if one term is less than another in KBO.twee-lib8Check if one term is less than another in a given model. Safe-Inferred"%&Stwee-libA critical pair together with information about how it was derivedtwee-libThe critical pair itself.twee-libThe critical term, if there is one. (Axioms do not have a critical term.)twee-lib2A derivation of the critical pair from the axioms.twee-lib(?(@(A(B(C(D(E(F(G(H(I(J(K(L(M(N(O(P(Q(R(S(T(U(V(W(X(Y(Z([\]\^\_\`\a\b\c\d\d\e\f\g\h\i\jklmnopqrstuvwxyz{|}~{nP                                                                                                                                                                     kz( %twee-lib-2.4.2-1ARvabPuymzCxoMgVx1SPC Twee.Pretty Data.Label Twee.Profile Twee.Task Twee.Term Twee.UtilsTwee.Constraints Twee.Base Twee.Index Twee.Equation Twee.Proof Twee.RuleTwee.Rule.IndexTwee.KBOTwee.CP Twee.JoinTweeData.ChurchListData.DynamicArray Data.Heap Data.NumberedData.PackedSequenceData.BatchedQueueTwee.Term.CoreunpackScoreCPRulesplitpretty-1.1.3.6Text.PrettyPrint.HughesPJClass PrettyLevel pPrintPrec pPrintListpPrintPretty prettyShow prettyParen prettyNormalText.PrettyPrint.HughesPJDoc zeroWidthTextvcattextspace sizedTextsepsemirparen renderStylerender reduceDocrbrackrbracerationalquotes punctuateptextparensnest maybeQuotes maybeParensmaybeDoubleQuotes maybeBrackets maybeBraceslparenlbracklbraceisEmptyintegerinthsephcathang fullRenderfsepfloatfirstfcatequals doubleQuotesdoublecommacoloncharcatbracketsbraces<+>$+$$$#Text.PrettyPrint.Annotated.HughesPJStrPStrChr TextDetailsribbonsPerLinemode lineLengthStyle ZigZagModePageMode OneLineModeLeftModeModestyleLabellabelNum unsafeMkLabellabelfind $fEqLabel $fOrdLabel $fShowLabelstamp stampWithstampMprofileTasknewTask checkTaskBuilderVarVvar_idFunfun_idTermTermListApp UnsafeConsSymuhdutlurestConsSymhdtlrest UnsafeConsConsEmptyatlenList singletonisSubtermOfListU16U8SamplerepeatM partitionBycollateisSorted isSortedByusortusortBysortBy'usortBy'orElse unbufferedlabelMfixpoint fixpointOnintMinintMax splitInterval reservoir emptySample addSample sampleValue mapSamplesplitsfoldnnever $fSerializeU8$fSerializeU16$fEqU16$fOrdU16$fNumU16 $fRealU16 $fEnumU16 $fIntegralU16$fEqU8$fOrdU8$fNumU8$fRealU8$fEnumU8 $fIntegralU8Labelled TriangleSubstTriangle unTriangleSubstunSubst SubstitutionSubstFun evalSubst substListBuildBuildFunbuilderFbuild buildListconappvar substToList foldSubstallSubst substDomainsubst substSize lookupList extendListretractunsafeExtendListsubstCompatible substUnion idempotent idempotentOnclose canonicalise emptySubstemptyTriangleSubst listToSubstmatchmatchIn matchList matchListIn matchMany matchManyIn matchManyListmatchManyListInunify unifyList unifyMany unifyManyTriunifyTri unifyTriFrom unifyListTriunifyListTriFromemptychildrenlookupextendlenbound boundList boundListsoccurs subtermsListsubtermsreverseSubtermsListreverseSubtermsproperSubtermsisAppisVar isInstanceOf isVariantOf isSubtermOfmapFun mapFunListreplacereplacePositionreplacePositionSubpositionToPathpathToPosition<<fun fun_value $fBuild[]$fBuildTermList $fBuildTerm$fBuildBuilder$fSubstitutionFUN$fSubstitutionSubst$fSubstitutionTriangleSubst $fShowFun $fShowSubst$fShowTermList $fShowTerm$fShowTriangleSubst $fEqSubst $fOrdSubst TermStyle pPrintTerm PrettyTerm termStyleANSICodeHighlightedTerm prettyPrint<#> pPrintEmpty pPrintTuple pPrintSetsupplygreenbold highlightmaybeHighlight invisiblecurried uncurried fixedArityimplicitArgumentsprefixpostfix infixStyle tupleStyle $fPrettyFun $fPrettyRatio $fPrettyMap $fPrettyVar $fPrettySet $fPrettyDoc $fPrettySubst$fPrettyTermList$fPrettyHighlightedTerm $fPrettyTerm StrictnessStrict NonstrictOrderedlessEqlessIn lessEqSkolemMinimalminimalModelBranchfunslessFormulaLessLessEqAndOrAtomConstantVariableatomstoTermfromTerm negateFormulaconjdisj&&&|||truefalse trueBranchnorm contradictoryformAndbranchesaddLess addEqualsaddTermmodelToLiteralsmodelFromOrder weakenModel varInModel varGroups lessEqInModelsolvelessThan orientTerms $fPrettyAtom$fPrettyFormula$fPrettyBranch $fPrettyModel$fEqStrictness$fShowStrictness $fEqModel $fShowModel $fEqBranch $fOrdBranch $fEqFormula $fOrdFormula $fShowFormula $fShowAtom$fEqAtom $fOrdAtom EqualsBonushasEqualsBonusisEqualsisTrueisFalseFunctionHastheFunOf BuilderOfTriangleSubstOfSubstOf TermListOfTermOfSymbolic ConstantOftermsDLsubst_IdunIdtermsvarsisGroundoccoccVarrenameAvoidingfreshVarrenameManyAvoiding isMinimal minimalTermerase eraseExceptground $fPrettyId$fSymbolicMaybe $fSymbolic[]$fSymbolic(,,) $fSymbolic(,)$fSymbolicSubst$fSymbolicTermList$fSymbolicTerm$fEqualsBonusFun$fEqId$fOrdId$fShowId$fEnumId $fBoundedId$fNumId$fRealId $fIntegralId $fSerializeIdIndex invariantnullinsertdeletematcheselemsfromList fromListWith$fDefaultIndex $fShowIndex EquationOfEquation:=:eqn_lhseqn_rhsorderorderedSimplerThan bothSidestrivial simplerThan matchEquation$fPrettyEquation$fSymbolicEquation $fEqEquation $fOrdEquation$fShowEquation ProvedGoal pg_numberpg_namepg_proof pg_goal_hintpg_witness_hint Presentation pres_axioms pres_lemmas pres_goalsConfigcfg_all_lemmas cfg_no_lemmascfg_ground_proofcfg_show_instancescfg_use_colourcfg_show_uses_of_axiomsAxiom axiom_number axiom_name axiom_eqn DerivationUseLemmaUseAxiomReflSymmTransCongProofequation derivationcertifylemma simpleLemmaaxiom autoSubstsymmtranscongsimplifysteps usedLemmasusedLemmasAndSubsts usedAxiomsusedAxiomsAndSubstsgroundAxiomsAndSubstseliminateDefinitionsFromGoaleliminateDefinitionscongPath defaultConfig provedGoalcheckProvedGoalpresentpPrintPresentationdescribeEquation $fPrettyAxiom$fPrettyDerivation $fPrettyProof$fSymbolicDerivation $fOrdProof $fEqProof$fPrettyPresentation$fShowPresentation$fShowProvedGoal$fEqDerivation$fShowDerivation $fShowProof $fEqAxiom $fOrdAxiom $fShowAxiom ReductionStrategy OrientationOrientedWeaklyOriented Permutative UnorientedRuleOf orientation rule_prooflhsrhsruleDerivationorientedunorientorient backwardssimplifyOutermostsimplifyInnermost simpleRewriteresultreductionProof ruleResult ruleProof normaliseWith normalForms successorssuccessorsAndNormalFormsanywhereanywhereOutermostanywhereInnermostrewritetryRule reducesWithreducesreducesOrientedreducesInModel reducesSkolem$fSymbolicOrientation$fOrdOrientation$fEqOrientation $fPrettyRule $fHasRuleTerm$fSymbolicRule $fHasRuleRule $fOrdRule$fEqRule $fShowRule$fShowOrientation RuleIndexindex_oriented index_all$fShowRuleIndexWeighted argWeightSizedsize $fSizedFun$fSizedEquation $fSizedTerm$fSizedTermList $fWeightedFun CriticalPaircp_eqncp_topcp_proof cfg_lhsweight cfg_rhsweight cfg_funweight cfg_varweightcfg_depthweight cfg_dupcost cfg_dupfactorDepth DirectionForwards BackwardsHowhow_poshow_dir1how_dir2Overlap overlap_rule1 overlap_rule2 overlap_how overlap_top overlap_eqn Positions2 ForwardsPosBothPos PositionsOf PositionsNilPConsP positions positionsRulepositionsChurchdirectoverlapsoverlapsChurch directionsasymmetricOverlaps overlapAt overlapAt'simplifyOverlapbuildReplacePositionSub termSubstscoremakeCriticalPair$fShowPositions$fSerializeHow$fPrettyCriticalPair$fSymbolicCriticalPair $fEqDepth $fOrdDepth $fNumDepth $fRealDepth $fEnumDepth$fIntegralDepth $fShowDepth $fShowOverlap$fEqHow$fOrdHow $fShowHow $fEqDirection$fOrdDirection$fEnumDirection$fShowDirectioncfg_ground_join cfg_use_connectedness_standalone'cfg_use_connectedness_in_ground_joining cfg_set_joinjoinCriticalPairallSteps checkOrderstep1step2step3joinWithsubsumed subsumed1 groundJoingroundJoinFromgroundJoinFromMaybevalidoptimiseOutputoutput_messageGoal goal_name goal_numbergoal_eqngoal_expanded_lhsgoal_expanded_rhsgoal_lhsgoal_rhsInfo info_depthinfo_maxActive active_id active_info active_rule active_top active_proof active_modelactive_positions BatchKindRule1Rule2Batch batch_kind batch_rule batch_best batch_restPassive passive_score passive_rule1 passive_rule2 passive_howMessage NewActive NewEquation DeleteActive SimplifyQueue NotComplete InterreduceStatusStatest_rules st_active_set st_joinablest_goalsst_queuest_next_active st_consideredst_simplified_at st_cp_samplest_not_complete st_completest_messages_revcfg_accept_termcfg_max_critical_pairscfg_max_cp_depth cfg_simplifycfg_renormalise_percentcfg_cp_sample_sizecfg_renormalise_thresholdcfg_set_join_goalscfg_always_simplifycfg_complete_subsetscfg_critical_pairscfg_joincfg_proof_presentationconfigIsComplete initialStatemessage clearMessagesmessages makePassives makePassive findPassivesimplifyPassiveshouldSimplifyQueue simplifyQueueenqueuedequeue active_cp activeRules addActivesample resetSamplesimplifySample addActiveOnly deleteActiveconsider considerUsingaddCPaddAxiom addJoinablecheckCompletenessassumeCompleteaddGoalnormaliseGoalsrecomputeGoals resetGoalrewriteGoalsBackwardsgoal interreduce interreduce1complete complete1solved solutionsrules completePure normaliseTerm simplifyTerm $fOrdPassive $fBatchBatch$fHasActivePositions2$fHasActiveRule$fHasActiveDepth $fHasActiveId$fPrettyActive $fEqActive$fPrettyMessage $fShowGoal $fEqBatchKind $fEqPassive ChurchListfoldretanilunitconsappendjointoListfoldl'filter fromMaybeArray arrayContentsDefaultdefnewArray!getWithDefaultupdate arrayStart arraySizeupdateWithDefaultHeapunion removeMinmapMaybebase GHC.MaybeNothingNumberedputmodifyPackedSequenceuncons StandardBatchEntry makeBatch unconsBatch batchLabel batchSizeQueueunbatchremoveMinFilter toBatchesGHC.BasememptymappendunsafeAt occursListBuilder1 unBuildertermlistroothighlowarraySymbolisFunindextoSymbol fromSymbol symbolSize unsafePatHeadpatHeadpatTermcompareSameLength buildTermListbuiltthen_emitSymbolBuilderemitAppemitVar emitTermListreserveunSTunIntsymbolOccursList<>ghc-prim GHC.TypesTrueJustLT dlist-1.0-BGLs0gqsZFwLq1Wa6dJ09jData.DList.InternalDList fromSteps