Index
| $$ | Theory.Text.Pretty |
| $-$ | Theory.Text.Pretty |
| $--$ | Theory.Text.Pretty |
| .&&. | Theory.Model.Formula, Theory.Model, Theory |
| .<=>. | Theory.Model.Formula, Theory.Model, Theory |
| .==>. | Theory.Model.Formula, Theory.Model, Theory |
| .||. | Theory.Model.Formula, Theory.Model, Theory |
| <-> | Theory.Text.Pretty |
| <> | Theory.Text.Pretty |
| AC | Theory.Model, Theory |
| ACSym | Theory.Model, Theory |
| Action | Theory.Model.Atom, Theory.Model, Theory |
| ActionG | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| addAxiom | Theory |
| addComment | Theory |
| addDisj | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| addEqs | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| addFormalComment | Theory |
| addFunSym | Theory.Model, Theory |
| addIntrRuleACs | Theory |
| addLemma | Theory |
| addProtoRule | Theory |
| addRuleVariants | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| addStringComment | Theory |
| addStRule | Theory.Model, Theory |
| All | Theory.Model.Formula, Theory.Model, Theory |
| allActions | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| allKDConcs | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| allKUActions | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| AllTraces | Theory |
| alwaysBefore | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| And | Theory.Model.Formula, Theory.Model, Theory |
| angled | Theory.Text.Parser.Token |
| AnnotatedGoal | Theory.Constraint.Solver.Goals |
| annotateProof | Theory.Proof, Theory |
| apBound | Theory.Proof, Theory |
| apCut | Theory.Proof, Theory |
| apHeuristic | Theory.Proof, Theory |
| Apply | Theory.Model, Theory |
| apply | Theory.Model, Theory |
| applyChangeList | Theory.Constraint.Solver.Reduction |
| applyLit | Theory.Model, Theory |
| applyPartialEvaluation | Theory |
| applySubst | Theory.Model, Theory |
| applyVTerm | Theory.Model, Theory |
| Arbitrary | Theory.Model, Theory |
| asymEncMaudeSig | Theory.Model, Theory |
| Ato | Theory.Model.Formula, Theory.Model, Theory |
| Atom | Theory.Model.Atom, Theory.Model, Theory |
| atomToGAtom | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| atPath | Theory.Proof, Theory |
| AutoProver | |
| 1 (Type/Class) | Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Proof, Theory |
| avoid | Theory.Model, Theory |
| AvoidInduction | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| avoidPrecise | Theory.Model, Theory |
| axFormula | Theory |
| Axiom | |
| 1 (Type/Class) | Theory |
| 2 (Data Constructor) | Theory |
| AxiomItem | Theory |
| axName | Theory |
| bindTerm | Theory.Model, Theory |
| BLAtom | Theory.Model.Atom, Theory.Model, Theory |
| BLTerm | Theory.Model, Theory |
| bltermNodeId | Theory.Model, Theory |
| bltermNodeId' | Theory.Model, Theory |
| BLVar | Theory.Model, Theory |
| BoringNodeStyle | Theory.Constraint.System.Dot |
| Bound | Theory.Model, Theory |
| bpFunSig | Theory.Model, Theory |
| bpIntruderRules | Theory.Tools.IntruderRules |
| bpMaudeSig | Theory.Model, Theory |
| bpReducibleFunSig | Theory.Model, Theory |
| braced | Theory.Text.Parser.Token |
| braces | Theory.Text.Pretty |
| brackets | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| BVar | Theory.Model, Theory |
| bvarToLVar | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| C | Theory.Model, Theory |
| CaseDistinction | |
| 1 (Type/Class) | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.Solver.Types |
| CaseDistKind | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| caseEmptyDoc | Theory.Text.Pretty |
| CaseName | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| cat | Theory.Text.Pretty |
| cdCases | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| cdGoal | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| ChainG | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Changed | Theory.Constraint.Solver.Reduction |
| ChangeIndicator | Theory.Constraint.Solver.Reduction |
| char | Theory.Text.Pretty |
| checkAndExtendProver | Theory.Proof, Theory |
| checkWellformedness | Theory.Tools.Wellformedness |
| children | Theory.Proof, Theory |
| ClassifiedRules | |
| 1 (Type/Class) | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| ClosedProtoRule | |
| 1 (Type/Class) | Theory |
| 2 (Data Constructor) | Theory |
| ClosedRuleCache | |
| 1 (Type/Class) | Theory |
| 2 (Data Constructor) | Theory |
| ClosedTheory | Theory |
| closeTheory | Theory |
| CoerceRule | Theory.Model.Rule, Theory.Model, Theory |
| colon | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| comma | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| commaSep | Theory.Text.Parser.Token |
| commaSep1 | Theory.Text.Parser.Token |
| Comment | Theory.Text.Pretty |
| comment | Theory.Text.Pretty |
| comment_ | Theory.Text.Pretty |
| CompactBoringNodes | Theory.Constraint.System.Dot |
| CompleteProof | Theory.Proof, Theory |
| compose | Theory.Model, Theory |
| composeVFresh | Theory.Model, Theory |
| compressSystem | Theory.Constraint.System.Dot |
| computeVariantsCached | Theory.Tools.RuleVariants |
| Con | Theory.Model, Theory |
| ConcIdx | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| Conj | |
| 1 (Data Constructor) | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Type/Class) | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| conjoinSystem | Theory.Constraint.Solver.Reduction |
| Conn | Theory.Model.Formula, Theory.Model, Theory |
| Connective | Theory.Model.Formula, Theory.Model, Theory |
| ConstrRule | Theory.Model.Rule, Theory.Model, Theory |
| constsVTerm | Theory.Model, Theory |
| constTerm | Theory.Model, Theory |
| containsPrivate | Theory.Model, Theory |
| Contradiction | |
| 1 (Type/Class) | Theory.Constraint.Solver.Contradictions, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| contradictionProver | Theory.Proof, Theory |
| contradictions | Theory.Constraint.Solver.Contradictions, Theory.Constraint.Solver, Theory.Proof, Theory |
| contradictorySystem | Theory.Constraint.Solver.Contradictions |
| cprRuleE | Theory |
| crConstruct | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| crDestruct | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| crProtocol | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| CSym | Theory.Model, Theory |
| CurrentlyDeducible | Theory.Constraint.Solver.Goals |
| CutBFS | Theory.Proof, Theory |
| CutDFS | Theory.Proof, Theory |
| CutNothing | Theory.Proof, Theory |
| Cyclic | Theory.Constraint.Solver.Contradictions |
| DedFact | Theory.Model.Fact, Theory.Model, Theory |
| dedFactView | Theory.Model.Fact, Theory.Model, Theory |
| dedLogFact | Theory.Model.Fact, Theory.Model, Theory |
| defaultOpenTheory | Theory |
| defaultStyle | Theory.Text.Pretty |
| DelayedMatches | Theory.Model, Theory |
| DestrRule | Theory.Model.Rule, Theory.Model, Theory |
| dhFunSig | Theory.Model, Theory |
| dhIntruderRules | Theory.Tools.IntruderRules |
| dhMaudeSig | Theory.Model, Theory |
| dhReducibleFunSig | Theory.Model, Theory |
| DirTag | Theory.Model.Fact, Theory.Model, Theory |
| Disj | |
| 1 (Data Constructor) | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Type/Class) | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| DisjG | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| DnK | Theory.Model.Fact, Theory.Model, Theory |
| Doc | Theory.Text.Pretty |
| Document | Theory.Text.Pretty |
| dom | Theory.Model, Theory |
| domVFresh | Theory.Model, Theory |
| dot | Theory.Text.Parser.Token |
| dotSystemCompact | Theory.Constraint.System.Dot |
| dotSystemLoose | Theory.Constraint.System.Dot |
| double | Theory.Text.Pretty |
| doubleQuoted | Theory.Text.Parser.Token |
| doubleQuotes | Theory.Text.Pretty |
| dropNameHintsBound | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Edge | |
| 1 (Type/Class) | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| EMap | Theory.Model, Theory |
| emapSymString | Theory.Model, Theory |
| emptyClassifiedRules | Theory.Constraint.Solver.Types |
| emptyDoc | Theory.Text.Pretty |
| emptyEqStore | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| emptySignaturePure | Theory.Model.Signature, Theory.Model, Theory |
| emptySubst | Theory.Model, Theory |
| emptySubstVFresh | Theory.Model, Theory |
| emptySystem | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| enableBP | Theory.Model, Theory |
| enableDH | Theory.Model, Theory |
| enableMSet | Theory.Model, Theory |
| enumConcs | Theory.Model.Rule, Theory.Model, Theory |
| enumPrems | Theory.Model.Rule, Theory.Model, Theory |
| EqE | Theory.Model.Atom, Theory.Model, Theory |
| eqLHS | Theory.Model, Theory |
| eqModuloFreshnessNoAC | Theory.Model, Theory |
| eqRHS | Theory.Model, Theory |
| eqsConj | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| eqsIsFalse | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| eqsSubst | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| EqStore | |
| 1 (Type/Class) | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Equal | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| equals | Theory.Text.Pretty |
| equalSign | Theory.Text.Parser.Token |
| eSrc | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| eTgt | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| evalEqual | Theory.Model, Theory |
| evalFreshAvoiding | Theory.Model, Theory |
| evalFreshTAvoiding | Theory.Model, Theory |
| EvaluationStyle | Theory.Tools.AbstractInterpretation |
| Ex | Theory.Model.Formula, Theory.Model, Theory |
| execProofMethod | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| execReduction | Theory.Constraint.Solver.Reduction |
| exists | Theory.Model.Formula, Theory.Model, Theory |
| ExistsNoTrace | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| ExistsSomeTrace | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| ExistsTrace | Theory |
| expSym | Theory.Model, Theory |
| expSymString | Theory.Model, Theory |
| extendWithRenaming | Theory.Model, Theory |
| Fact | |
| 1 (Type/Class) | Theory.Model.Fact, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Fact, Theory.Model, Theory |
| factArity | Theory.Model.Fact, Theory.Model, Theory |
| factMultiplicity | Theory.Model.Fact, Theory.Model, Theory |
| FactTag | Theory.Model.Fact, Theory.Model, Theory |
| factTag | Theory.Model.Fact, Theory.Model, Theory |
| factTagArity | Theory.Model.Fact, Theory.Model, Theory |
| factTagMultiplicity | Theory.Model.Fact, Theory.Model, Theory |
| factTagName | Theory.Model.Fact, Theory.Model, Theory |
| factTerms | Theory.Model.Fact, Theory.Model, Theory |
| falseEqConstrConj | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| FApp | Theory.Model, Theory |
| fApp | Theory.Model, Theory |
| fAppAC | Theory.Model, Theory |
| FAppC | Theory.Model, Theory |
| fAppC | Theory.Model, Theory |
| fAppEMap | Theory.Model, Theory |
| fAppExp | Theory.Model, Theory |
| fAppFst | Theory.Model, Theory |
| fAppInv | Theory.Model, Theory |
| fAppList | Theory.Model, Theory |
| FAppNoEq | Theory.Model, Theory |
| fAppNoEq | Theory.Model, Theory |
| fAppOne | Theory.Model, Theory |
| fAppPair | Theory.Model, Theory |
| fAppPMult | Theory.Model, Theory |
| fAppSnd | Theory.Model, Theory |
| fcat | Theory.Text.Pretty |
| FEMap | Theory.Model, Theory |
| FExp | Theory.Model, Theory |
| FInv | Theory.Model, Theory |
| fixedWidthText | Theory.Text.Pretty |
| flattenMatch | Theory.Model, Theory |
| FList | Theory.Model, Theory |
| float | Theory.Text.Pretty |
| fmapTerm | Theory.Model, Theory |
| FMult | Theory.Model, Theory |
| focus | Theory.Proof, Theory |
| foldBVar | Theory.Model, Theory |
| foldFormula | Theory.Model.Formula, Theory.Model, Theory |
| foldFrees | Theory.Model, Theory |
| foldFreesOcc | Theory.Model, Theory |
| foldProof | Theory.Proof, Theory |
| forall | Theory.Model.Formula, Theory.Model, Theory |
| ForbiddenBP | Theory.Constraint.Solver.Contradictions |
| ForbiddenExp | Theory.Constraint.Solver.Contradictions |
| ForbiddenKD | Theory.Constraint.Solver.Contradictions |
| formalComment | Theory.Text.Parser.Token |
| Formula | Theory.Model.Formula, Theory.Model, Theory |
| FormulasFalse | Theory.Constraint.Solver.Contradictions |
| formulaToGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| formulaToGuarded_ | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| formulaToSystem | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| FPair | Theory.Model, Theory |
| FPMult | Theory.Model, Theory |
| Free | Theory.Model, Theory |
| frees | Theory.Model, Theory |
| freesList | Theory.Model, Theory |
| freeToFreshRaw | Theory.Model, Theory |
| FreshConstrRule | Theory.Model.Rule, Theory.Model, Theory |
| FreshFact | Theory.Model.Fact, Theory.Model, Theory |
| freshFact | Theory.Model.Fact, Theory.Model, Theory |
| freshLVar | Theory.Model, Theory |
| FreshName | Theory.Model, Theory |
| freshName | Theory.Text.Parser.Token |
| FreshRule | Theory.Model.Rule, Theory.Model, Theory |
| freshTerm | Theory.Model, Theory |
| freshToFree | Theory.Model, Theory |
| freshToFreeAvoiding | Theory.Model, Theory |
| freshToFreeAvoidingFast | Theory.Model, Theory |
| fromFree | Theory.Model, Theory |
| fsep | Theory.Text.Pretty |
| fsepList | Theory.Text.Pretty |
| FullBoringNodes | Theory.Constraint.System.Dot |
| FUnion | Theory.Model, Theory |
| FunSig | Theory.Model, Theory |
| FunSym | Theory.Model, Theory |
| funSyms | Theory.Model, Theory |
| GAction | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gall | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GAto | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GAtom | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GConj | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gconj | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GDisj | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gdisj | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GEqE | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| getCaseDistinction | Theory |
| getClassifiedRules | Theory |
| getConcIdx | Theory.Model.Rule, Theory.Model, Theory |
| getConj | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| getDisj | Theory.Constraint.Solver.Reduction, Theory.Constraint.Solver, Theory.Proof, Theory |
| getInjectiveFactInsts | Theory |
| getIntrVariants | Theory |
| getLemmas | Theory |
| getMaudeHandle | Theory.Constraint.Solver.Reduction |
| getMaudeStats | Theory.Model, Theory |
| getNameId | Theory.Model, Theory |
| getPremIdx | Theory.Model.Rule, Theory.Model, Theory |
| getProofContext | |
| 1 (Function) | Theory.Constraint.Solver.Reduction |
| 2 (Function) | Theory |
| getProtoRuleEs | Theory |
| gex | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gfalse | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| ginduct | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gnot | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Goal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| GoalNrRanking | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| GoalRanking | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| goalRankingName | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| GoalStatus | |
| 1 (Type/Class) | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gsLoopBreaker | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gsNr | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gsSolved | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| gtrue | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Guarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| guardFactTags | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| hang | Theory.Text.Pretty |
| HasFrees | Theory.Model, Theory |
| hashMaudeSig | Theory.Model, Theory |
| HasRuleName | Theory.Model.Rule, Theory.Model, Theory |
| hcat | Theory.Text.Pretty |
| Heuristic | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| highlight | Theory.Text.Pretty |
| HighlightDocument | Theory.Text.Pretty |
| HighlightStyle | Theory.Text.Pretty |
| hsep | Theory.Text.Pretty |
| identifier | Theory.Text.Parser.Token |
| Iff | Theory.Model.Formula, Theory.Model, Theory |
| imageOf | Theory.Model, Theory |
| imageOfVFresh | Theory.Model, Theory |
| Imp | Theory.Model.Formula, Theory.Model, Theory |
| implicitFunSig | Theory.Model, Theory |
| ImpossibleChain | Theory.Constraint.Solver.Contradictions |
| IncompatibleEqs | Theory.Constraint.Solver.Contradictions |
| IncompleteProof | Theory.Proof, Theory |
| IncrementalProof | Theory.Proof, Theory |
| indexedIdentifier | Theory.Text.Parser.Token |
| Induction | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| InductionHint | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| InFact | Theory.Model.Fact, Theory.Model, Theory |
| inFact | Theory.Model.Fact, Theory.Model, Theory |
| insertAction | Theory.Constraint.Solver.Reduction |
| insertAtom | Theory.Constraint.Solver.Reduction |
| insertChain | Theory.Constraint.Solver.Reduction |
| insertEdges | Theory.Constraint.Solver.Reduction |
| insertFormula | Theory.Constraint.Solver.Reduction |
| insertFreshNode | Theory.Constraint.Solver.Reduction |
| insertFreshNodeConc | Theory.Constraint.Solver.Reduction |
| insertGoal | Theory.Constraint.Solver.Reduction |
| insertLemmas | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| insertLess | Theory.Constraint.Solver.Reduction |
| insertPaths | Theory.Proof, Theory |
| int | Theory.Text.Pretty |
| integer | Theory.Text.Pretty |
| interpretAbstractly | Theory.Tools.AbstractInterpretation |
| IntrInfo | Theory.Model.Rule, Theory.Model, Theory |
| IntrRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| IntrRuleACInfo | Theory.Model.Rule, Theory.Model, Theory |
| InvariantLemma | Theory |
| invSymString | Theory.Model, Theory |
| IRecvRule | Theory.Model.Rule, Theory.Model, Theory |
| irreducibleFunSyms | Theory.Model, Theory |
| isActionAtom | Theory.Model.Atom, Theory.Model, Theory |
| isActionGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isAllGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isChainGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isCoerceRule | Theory.Model.Rule, Theory.Model, Theory |
| isConjunction | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| IsConst | Theory.Model, Theory |
| isConstrRule | Theory.Model.Rule, Theory.Model, Theory |
| isDEMapRule | Theory.Tools.IntruderRules |
| isDestrRule | Theory.Model.Rule, Theory.Model, Theory |
| isDExpRule | Theory.Tools.IntruderRules |
| isDisjGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isDisjunction | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isDPMultRule | Theory.Tools.IntruderRules |
| isEMap | Theory.Model, Theory |
| isEmpty | Theory.Text.Pretty |
| ISendRule | Theory.Model.Rule, Theory.Model, Theory |
| isEqAtom | Theory.Model.Atom, Theory.Model, Theory |
| isExGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isFreshRule | Theory.Model.Rule, Theory.Model, Theory |
| isFreshVar | Theory.Model, Theory |
| isInTrace | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isIntruderRule | Theory.Model.Rule, Theory.Model, Theory |
| isInverse | Theory.Model, Theory |
| isIRecvRule | Theory.Model.Rule, Theory.Model, Theory |
| isISendRule | Theory.Model.Rule, Theory.Model, Theory |
| isKDFact | Theory.Model.Fact, Theory.Model, Theory |
| isKFact | Theory.Model.Fact, Theory.Model, Theory |
| isKUFact | Theory.Model.Fact, Theory.Model, Theory |
| isLast | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isLastAtom | Theory.Model.Atom, Theory.Model, Theory |
| isLessAtom | Theory.Model.Atom, Theory.Model, Theory |
| isLinearFact | Theory.Model.Fact, Theory.Model, Theory |
| isMsgVar | Theory.Model, Theory |
| isNullaryPublicFunction | Theory.Model, Theory |
| isPair | Theory.Model, Theory |
| isPersistentFact | Theory.Model.Fact, Theory.Model, Theory |
| isPremiseGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isPrivateFunction | Theory.Model, Theory |
| isProduct | Theory.Model, Theory |
| isProtoFact | Theory.Model.Fact, Theory.Model, Theory |
| isRenaming | Theory.Model, Theory |
| isSafetyFormula | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isSimpleTerm | Theory.Model, Theory |
| isSplitGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isStandardActionGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| isTrivialProtoVariantAC | Theory.Model.Rule, Theory.Model, Theory |
| isUnion | Theory.Model, Theory |
| IsVar | Theory.Model, Theory |
| isVar | Theory.Model, Theory |
| joinAllRules | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| KDFact | Theory.Model.Fact, Theory.Model, Theory |
| kdFact | Theory.Model.Fact, Theory.Model, Theory |
| Keyword | Theory.Text.Pretty |
| keyword | Theory.Text.Pretty |
| keyword_ | Theory.Text.Pretty |
| kFactView | Theory.Model.Fact, Theory.Model, Theory |
| kLogFact | Theory.Model.Fact, Theory.Model, Theory |
| kuActionAtoms | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| KUFact | Theory.Model.Fact, Theory.Model, Theory |
| kuFact | Theory.Model.Fact, Theory.Model, Theory |
| kwAxiom | Theory.Text.Pretty |
| kwBy | Theory.Text.Pretty |
| kwCase | Theory.Text.Pretty |
| kwEnd | Theory.Text.Pretty |
| kwInstanceModulo | Theory.Text.Pretty |
| kwLemma | Theory.Text.Pretty |
| kwModulo | Theory.Text.Pretty |
| kwNext | Theory.Text.Pretty |
| kwQED | Theory.Text.Pretty |
| kwRuleModulo | Theory.Text.Pretty |
| kwTheoryHeader | Theory.Text.Pretty |
| kwTypesModulo | Theory.Text.Pretty |
| kwVariantsModulo | Theory.Text.Pretty |
| labelNodeId | Theory.Constraint.Solver.Reduction |
| Last | Theory.Model.Atom, Theory.Model, Theory |
| lAttributes | Theory |
| lbrace | Theory.Text.Pretty |
| lbrack | Theory.Text.Pretty |
| LeftMode | Theory.Text.Pretty |
| Lemma | Theory |
| LemmaAttribute | Theory |
| LemmaItem | Theory |
| Less | |
| 1 (Data Constructor) | Theory.Model.Atom, Theory.Model, Theory |
| 2 (Type/Class) | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| LFact | Theory.Model.Fact, Theory.Model, Theory |
| lfalse | Theory.Model.Formula, Theory.Model, Theory |
| LFormula | Theory.Model.Formula, Theory.Model, Theory |
| lFormula | Theory |
| LGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Linear | Theory.Model.Fact, Theory.Model, Theory |
| lineComment | Theory.Text.Pretty |
| lineComment_ | Theory.Text.Pretty |
| lineLength | Theory.Text.Pretty |
| List | Theory.Model, Theory |
| list | Theory.Text.Parser.Token |
| Lit | |
| 1 (Type/Class) | Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model, Theory |
| lit | Theory.Model, Theory |
| Lit2 | Theory.Model, Theory |
| lits | Theory.Model, Theory |
| lName | Theory |
| LNAtom | Theory.Model.Atom, Theory.Model, Theory |
| LNFact | Theory.Model.Fact, Theory.Model, Theory |
| LNFormula | Theory.Model.Formula, Theory.Model, Theory |
| LNGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| LNode | Theory.Proof, Theory |
| LNSubst | Theory.Model, Theory |
| LNSubstVFresh | Theory.Model, Theory |
| LNTerm | Theory.Model, Theory |
| lookupConc | Theory.Model.Rule, Theory.Model, Theory |
| lookupLemma | Theory |
| lookupLemmaProof | Theory |
| lookupPrem | Theory.Model.Rule, Theory.Model, Theory |
| LoopBreaker | Theory.Constraint.Solver.Goals |
| lparen | Theory.Text.Pretty |
| lProof | Theory |
| LSort | Theory.Model, Theory |
| LSortFresh | Theory.Model, Theory |
| LSortMsg | Theory.Model, Theory |
| LSortNode | Theory.Model, Theory |
| LSortPub | Theory.Model, Theory |
| LSubst | Theory.Model, Theory |
| LSubstVFresh | Theory.Model, Theory |
| LTerm | Theory.Model, Theory |
| ltermNodeId | Theory.Model, Theory |
| ltermNodeId' | Theory.Model, Theory |
| ltermVar | Theory.Model, Theory |
| ltermVar' | Theory.Model, Theory |
| lTraceQuantifier | Theory |
| LTree | Theory.Proof, Theory |
| ltrue | Theory.Model.Formula, Theory.Model, Theory |
| LVar | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| lvar | Theory.Text.Parser.Token |
| lvarIdx | Theory.Model, Theory |
| lvarName | Theory.Model, Theory |
| lvarSort | Theory.Model, Theory |
| mapAtoms | Theory.Model.Formula, Theory.Model, Theory |
| mapFrees | Theory.Model, Theory |
| mapGuardedAtoms | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| mapProofInfo | Theory.Proof, Theory |
| mapProverProof | Theory.Proof, Theory |
| mapRange | Theory.Model, Theory |
| mapRangeVFresh | Theory.Model, Theory |
| markGoalAsSolved | Theory.Constraint.Solver.Reduction |
| Match | Theory.Model, Theory |
| matchFact | Theory.Model.Fact, Theory.Model, Theory |
| matchLVar | Theory.Model, Theory |
| matchOnlyIf | Theory.Model, Theory |
| matchWith | Theory.Model, Theory |
| MaudeHandle | Theory.Model, Theory |
| MaudeSig | Theory.Model, Theory |
| mergeMapsWith | Theory.Proof, Theory |
| mhFilePath | Theory.Model, Theory |
| mhMaudeSig | Theory.Model, Theory |
| minimalMaudeSig | Theory.Model, Theory |
| mkDUnionRule | Theory.Tools.IntruderRules |
| Mode | Theory.Text.Pretty |
| mode | Theory.Text.Pretty |
| modifyLemmaProof | Theory |
| Monotone | Theory.Model, Theory |
| MonotoneFunction | Theory.Model, Theory |
| msetFunSig | Theory.Model, Theory |
| msetMaudeSig | Theory.Model, Theory |
| msgvar | Theory.Text.Parser.Token |
| Mult | Theory.Model, Theory |
| multiComment | Theory.Text.Pretty |
| multiComment_ | Theory.Text.Pretty |
| Multiplicity | Theory.Model.Fact, Theory.Model, Theory |
| multisetIntruderRules | Theory.Tools.IntruderRules |
| Name | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| NameId | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| NameTag | Theory.Model, Theory |
| NAtom | Theory.Model.Atom, Theory.Model, Theory |
| natural | Theory.Text.Parser.Token |
| naturalSubscript | Theory.Text.Parser.Token |
| nest | Theory.Text.Pretty |
| nestBetween | Theory.Text.Pretty |
| nestShort | Theory.Text.Pretty |
| nestShort' | Theory.Text.Pretty |
| nestShortNonEmpty | Theory.Text.Pretty |
| nestShortNonEmpty' | Theory.Text.Pretty |
| neverContainsFreshPriv | Theory.Model, Theory |
| NFact | Theory.Model.Fact, Theory.Model, Theory |
| nfRule | Theory.Model.Rule, Theory.Model, Theory |
| nId | Theory.Model, Theory |
| niFactors | Theory.Model, Theory |
| NodeAfterLast | Theory.Constraint.Solver.Contradictions |
| NodeConc | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodeConcFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodeConcNode | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| NodeId | Theory.Model, Theory |
| NodePrem | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodePremFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodePremNode | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodeRule | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| nodevar | Theory.Text.Parser.Token |
| NoEq | Theory.Model, Theory |
| NoEqFunSig | Theory.Model, Theory |
| noEqFunSyms | Theory.Model, Theory |
| NoEqSym | Theory.Model, Theory |
| NoMatch | Theory.Model, Theory |
| nonEmptyGraph | Theory.Constraint.System.Dot |
| NonInjectiveFactInstance | Theory.Constraint.Solver.Contradictions |
| NonNormalTerms | Theory.Constraint.Solver.Contradictions |
| nonSilentRules | Theory.Constraint.Solver.Types |
| normalizeTheory | Theory |
| Not | Theory.Model.Formula, Theory.Model, Theory |
| noteWellformedness | Theory.Tools.Wellformedness |
| nTag | Theory.Model, Theory |
| NTerm | Theory.Model, Theory |
| numbered | Theory.Text.Pretty |
| numbered' | Theory.Text.Pretty |
| occurs | Theory.Model, Theory |
| occursVTerm | Theory.Model, Theory |
| One | Theory.Model, Theory |
| OneLineMode | Theory.Text.Pretty |
| oneStepProver | Theory.Proof, Theory |
| opAction | Theory.Text.Pretty |
| opAt | Theory.Text.Parser.Token |
| opBang | Theory.Text.Parser.Token |
| opChain | Theory.Text.Parser.Token |
| opDedBefore | Theory.Text.Pretty |
| opDot | Theory.Text.Pretty |
| opEdge | Theory.Text.Pretty |
| openFormula | Theory.Model.Formula, Theory.Model, Theory |
| openFormulaPrefix | Theory.Model.Formula, Theory.Model, Theory |
| openGoals | Theory.Constraint.Solver.Goals |
| openGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| OpenTheory | Theory |
| openTheory | Theory |
| opEqual | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| Operator | Theory.Text.Pretty |
| operator | Theory.Text.Pretty |
| operator_ | Theory.Text.Pretty |
| opExists | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opExp | Theory.Text.Parser.Token |
| opForall | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opIff | Theory.Text.Pretty |
| opImp | Theory.Text.Pretty |
| opImplies | Theory.Text.Parser.Token |
| opLAnd | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLeftarrow | Theory.Text.Parser.Token |
| opLEquiv | Theory.Text.Parser.Token |
| opLess | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLFalse | Theory.Text.Parser.Token |
| opLNot | Theory.Text.Parser.Token |
| opLongleftarrow | Theory.Text.Parser.Token |
| opLongrightarrow | Theory.Text.Parser.Token |
| opLOr | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opLTrue | Theory.Text.Parser.Token |
| opMinus | Theory.Text.Parser.Token |
| opMult | Theory.Text.Parser.Token |
| opParens | Theory.Text.Pretty |
| opPath | Theory.Text.Pretty |
| opPlus | Theory.Text.Parser.Token |
| opProvides | Theory.Text.Pretty |
| opRequires | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| opRightarrow | Theory.Text.Parser.Token |
| opSharp | Theory.Text.Parser.Token |
| opSlash | Theory.Text.Parser.Token |
| Or | Theory.Model.Formula, Theory.Model, Theory |
| orelse | Theory.Proof, Theory |
| OutFact | Theory.Model.Fact, Theory.Model, Theory |
| outFact | Theory.Model.Fact, Theory.Model, Theory |
| PageMode | Theory.Text.Pretty |
| pairFunSig | Theory.Model, Theory |
| pairMaudeSig | Theory.Model, Theory |
| parens | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| parLTreeDFS | Theory.Proof, Theory |
| parseFile | Theory.Text.Parser.Token |
| parseIntruderRules | Theory.Text.Parser |
| parseLemma | Theory.Text.Parser |
| parseOpenTheory | Theory.Text.Parser |
| parseOpenTheoryString | Theory.Text.Parser |
| Parser | Theory.Text.Parser.Token |
| parseString | Theory.Text.Parser.Token |
| partialEvaluation | Theory.Tools.AbstractInterpretation |
| pcCaseDistKind | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcCaseDists | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcInjectiveFactInsts | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcMaudeHandle | Theory.Constraint.Solver.Types |
| pcRules | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcSignature | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcTraceQuantifier | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| pcUseInduction | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| performSplit | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Persistent | Theory.Model.Fact, Theory.Model, Theory |
| pmultSym | Theory.Model, Theory |
| pmultSymString | Theory.Model, Theory |
| praciLoopBreakers | Theory.Model.Rule, Theory.Model, Theory |
| praciName | Theory.Model.Rule, Theory.Model, Theory |
| pracLoopBreakers | Theory.Model.Rule, Theory.Model, Theory |
| pracName | Theory.Model.Rule, Theory.Model, Theory |
| pracVariants | Theory.Model.Rule, Theory.Model, Theory |
| precomputeCaseDistinctions | Theory.Constraint.Solver.CaseDistinctions, Theory.Constraint.Solver, Theory.Proof, Theory |
| PremIdx | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| PremiseG | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyAxiom | Theory |
| prettyCaseDistinction | Theory.Constraint.Solver.Types |
| prettyClosedSummary | Theory |
| prettyClosedTheory | Theory |
| prettyContradiction | Theory.Constraint.Solver.Contradictions |
| prettyDisjLNSubstsVFresh | Theory.Model, Theory |
| prettyEdge | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyEqStore | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyFact | Theory.Model.Fact, Theory.Model, Theory |
| prettyFormalComment | Theory |
| prettyGoal | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyIntrRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| prettyIntrRuleACInfo | Theory.Model.Rule, Theory.Model, Theory |
| prettyIntruderVariants | Theory |
| prettyLemma | Theory |
| prettyLemmaName | Theory |
| prettyLess | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyLNFact | Theory.Model.Fact, Theory.Model, Theory |
| prettyLNFormula | Theory.Model.Formula, Theory.Model, Theory |
| prettyLNSubst | Theory.Model, Theory |
| prettyLNTerm | Theory.Model, Theory |
| prettyLoopBreakers | Theory.Model.Rule, Theory.Model, Theory |
| prettyLSubstVFresh | Theory.Model, Theory |
| prettyLVar | Theory.Model, Theory |
| prettyNAtom | Theory.Model.Atom, Theory.Model, Theory |
| prettyNFact | Theory.Model.Fact, Theory.Model, Theory |
| prettyNode | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyNodeConc | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyNodeId | Theory.Model, Theory |
| prettyNodePrem | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyNonGraphSystem | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyNTerm | Theory.Model, Theory |
| prettyOpenTheory | Theory |
| prettyProof | Theory.Proof, Theory |
| prettyProofMethod | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyProofWith | Theory.Proof, Theory |
| prettyProtoRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| prettyProtoRuleE | Theory.Model.Rule, Theory.Model, Theory |
| prettyProtoRuleName | Theory.Model.Rule, Theory.Model, Theory |
| prettyRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| prettyRuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| prettyRuleName | Theory.Model.Rule, Theory.Model, Theory |
| prettySignaturePure | Theory.Model.Signature, Theory.Model, Theory |
| prettySignatureWithMaude | Theory.Model.Signature, Theory.Model, Theory |
| prettySubst | Theory.Model, Theory |
| prettySubstVFresh | Theory.Model, Theory |
| prettySystem | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| prettyTerm | Theory.Model, Theory |
| prettyTraceQuantifier | Theory |
| prettyWfErrorReport | Theory.Tools.Wellformedness |
| Privacy | Theory.Model, Theory |
| Private | Theory.Model, Theory |
| ProbablyConstructible | Theory.Constraint.Solver.Goals |
| Proof | Theory.Proof, Theory |
| ProofContext | |
| 1 (Type/Class) | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| ProofMethod | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| ProofPath | Theory.Proof, Theory |
| ProofSkeleton | Theory |
| ProofStatus | Theory.Proof, Theory |
| ProofStep | |
| 1 (Type/Class) | Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Proof, Theory |
| proofStepStatus | Theory.Proof, Theory |
| ProtoFact | Theory.Model.Fact, Theory.Model, Theory |
| protoFact | Theory.Model.Fact, Theory.Model, Theory |
| ProtoInfo | Theory.Model.Rule, Theory.Model, Theory |
| ProtoRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| ProtoRuleACInfo | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| ProtoRuleACInstInfo | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| ProtoRuleE | Theory.Model.Rule, Theory.Model, Theory |
| ProtoRuleName | Theory.Model.Rule, Theory.Model, Theory |
| Prover | Theory.Proof, Theory |
| proveTheory | Theory |
| psInfo | Theory.Proof, Theory |
| psMethod | Theory.Proof, Theory |
| PubConstrRule | Theory.Model.Rule, Theory.Model, Theory |
| Public | Theory.Model, Theory |
| PubName | Theory.Model, Theory |
| pubName | Theory.Text.Parser.Token |
| pubTerm | Theory.Model, Theory |
| punctuate | Theory.Text.Pretty |
| Qua | Theory.Model.Formula, Theory.Model, Theory |
| Quantifier | Theory.Model.Formula, Theory.Model, Theory |
| quantify | Theory.Model.Formula, Theory.Model, Theory |
| quotes | Theory.Text.Pretty |
| rActs | Theory.Model.Rule, Theory.Model, Theory |
| range | Theory.Model, Theory |
| rangeVFresh | Theory.Model, Theory |
| rankProofMethods | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| rational | Theory.Text.Pretty |
| rawEdgeRel | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| rawLessRel | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| rbrace | Theory.Text.Pretty |
| rbrack | Theory.Text.Pretty |
| rConc | Theory.Model.Rule, Theory.Model, Theory |
| rConcs | Theory.Model.Rule, Theory.Model, Theory |
| reducibleFormula | Theory.Constraint.Solver.Reduction |
| Reduction | Theory.Constraint.Solver.Reduction |
| refineWithTypingAsms | Theory.Constraint.Solver.CaseDistinctions, Theory.Constraint.Solver, Theory.Proof, Theory |
| removeLemma | Theory |
| removeRedundantCases | Theory.Constraint.Solver.CaseDistinctions |
| removeRenamings | Theory.Model, Theory |
| removeSolvedSplitGoals | Theory.Constraint.Solver.Reduction |
| rename | Theory.Model, Theory |
| renameAvoiding | Theory.Model, Theory |
| renameDropNamehint | Theory.Model, Theory |
| renameFresh | Theory.Model, Theory |
| renameFreshAvoiding | Theory.Model, Theory |
| renamePrecise | Theory.Model, Theory |
| render | Theory.Text.Pretty |
| renderStyle | Theory.Text.Pretty |
| replaceSorryProver | Theory.Proof, Theory |
| reservedRuleNames | Theory.Model.Rule, Theory.Model, Theory |
| resolveNodeConcFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| resolveNodePremFact | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| restrict | Theory.Model, Theory |
| restrictVFresh | Theory.Model, Theory |
| ReuseLemma | Theory |
| ribbonsPerLine | Theory.Text.Pretty |
| rInfo | Theory.Model.Rule, Theory.Model, Theory |
| root | Theory.Proof, Theory |
| roundRobinHeuristic | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| rparen | Theory.Text.Pretty |
| rPrem | Theory.Model.Rule, Theory.Model, Theory |
| rPrems | Theory.Model.Rule, Theory.Model, Theory |
| RRule | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| rrulesForMaudeSig | Theory.Model, Theory |
| Rule | |
| 1 (Type/Class) | Theory.Model.Rule, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Rule, Theory.Model, Theory |
| RuleAC | Theory.Model.Rule, Theory.Model, Theory |
| RuleACConstrs | Theory.Model.Rule, Theory.Model, Theory |
| RuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| ruleACIntrToRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| ruleACIntrToRuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| ruleACToIntrRuleAC | Theory.Model.Rule, Theory.Model, Theory |
| RuleInfo | Theory.Model.Rule, Theory.Model, Theory |
| ruleInfo | Theory.Model.Rule, Theory.Model, Theory |
| RuleItem | Theory |
| ruleName | Theory.Model.Rule, Theory.Model, Theory |
| runAutoProver | Theory.Proof, Theory |
| runProver | Theory.Proof, Theory |
| runReduction | Theory.Constraint.Solver.Reduction |
| sCaseDistKind | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sConjDisjEqs | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sEdges | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| semi | Theory.Text.Pretty |
| sep | Theory.Text.Pretty |
| sEqStore | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sFormulas | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sGoals | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| showFactTag | Theory.Model.Fact, Theory.Model, Theory |
| showFactTagArity | Theory.Model.Fact, Theory.Model, Theory |
| showFunSymName | Theory.Model, Theory |
| showProofStatus | Theory.Proof, Theory |
| showRuleCaseName | Theory.Model.Rule, Theory.Model, Theory |
| sigmMaudeHandle | Theory.Model.Signature, Theory.Model, Theory |
| Signature | |
| 1 (Type/Class) | Theory.Model.Signature, Theory.Model, Theory |
| 2 (Data Constructor) | Theory.Model.Signature, Theory.Model, Theory |
| signatureMaudeSig | Theory.Model, Theory |
| SignaturePure | Theory.Model.Signature, Theory.Model, Theory |
| SignatureWithMaude | Theory.Model.Signature, Theory.Model, Theory |
| sigpMaudeSig | Theory.Model.Signature, Theory.Model, Theory |
| Silent | Theory.Tools.AbstractInterpretation |
| simp | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| simpDisjunction | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| simpleInjectiveFactInstances | Theory.Tools.InjectiveFactInstances |
| Simplify | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| simplifyGuarded | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| simplifySystem | Theory.Constraint.Solver.Simplify |
| singleQuoted | Theory.Text.Parser.Token |
| size | Theory.Model, Theory |
| Sized | Theory.Model, Theory |
| skeletonLemma | Theory |
| sLastAtom | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sLemmas | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sLessAtoms | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sMap | Theory.Model, Theory |
| SmartRanking | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| sNextGoalNr | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sNodes | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SolutionExtractor | Theory.Proof, Theory |
| Solved | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| solveFactEqs | Theory.Constraint.Solver.Reduction |
| SolveGoal | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| solveGoal | Theory.Constraint.Solver.Goals |
| solveMatchLNTerm | Theory.Model, Theory |
| solveMatchLTerm | Theory.Model, Theory |
| solveNodeIdEqs | Theory.Constraint.Solver.Reduction |
| solveRuleEqs | Theory.Constraint.Solver.Reduction |
| solveSubstEqs | Theory.Constraint.Solver.Reduction |
| solveTermEqs | Theory.Constraint.Solver.Reduction |
| solveWithCaseDistinction | Theory.Constraint.Solver.CaseDistinctions |
| someInst | Theory.Model, Theory |
| someRuleACInst | Theory.Model.Rule, Theory.Model, Theory |
| Sorry | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| sorry | Theory.Proof, Theory |
| sorryProver | Theory.Proof, Theory |
| sortCompare | Theory.Model, Theory |
| sortedLVar | Theory.Text.Parser.Token |
| sortGAtoms | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sortOfLit | Theory.Model, Theory |
| sortOfLNTerm | Theory.Model, Theory |
| sortOfLTerm | Theory.Model, Theory |
| sortOfName | Theory.Model, Theory |
| sortPrefix | Theory.Model, Theory |
| sortSuffix | Theory.Model, Theory |
| space | Theory.Text.Pretty |
| specialIntruderRules | Theory.Tools.IntruderRules |
| splitExists | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SplitG | Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SplitId | |
| 1 (Type/Class) | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| 2 (Data Constructor) | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SplitLater | Theory.Constraint.Solver.Reduction |
| SplitNow | Theory.Constraint.Solver.Reduction |
| splits | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| splitSize | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SplitStrategy | Theory.Constraint.Solver.Reduction |
| sSolvedFormulas | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| sSubst | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| standardActionAtoms | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| StandRule | Theory.Model.Rule, Theory.Model, Theory |
| startMaude | Theory.Model, Theory |
| stFunSyms | Theory.Model, Theory |
| stRules | Theory.Model, Theory |
| Style | |
| 1 (Data Constructor) | Theory.Text.Pretty |
| 2 (Type/Class) | Theory.Text.Pretty |
| Subst | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| substBound | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| substBoundAtom | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| substCreatesNonNormalTerms | Theory.Constraint.Solver.Contradictions |
| substEdges | Theory.Constraint.Solver.Reduction |
| substFormulas | Theory.Constraint.Solver.Reduction |
| substFree | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| substFreeAtom | Theory.Constraint.System.Guarded, Theory.Constraint.System.Constraints, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| substFromList | Theory.Model, Theory |
| substFromListVFresh | Theory.Model, Theory |
| substFromMap | Theory.Model, Theory |
| substLastAtom | Theory.Constraint.Solver.Reduction |
| substLessAtoms | Theory.Constraint.Solver.Reduction |
| substNodes | Theory.Constraint.Solver.Reduction |
| substSolvedFormulas | Theory.Constraint.Solver.Reduction |
| substSystem | Theory.Constraint.Solver.Reduction |
| substToList | Theory.Model, Theory |
| substToListOn | Theory.Model, Theory |
| substToListVFresh | Theory.Model, Theory |
| SubstVFresh | |
| 1 (Data Constructor) | Theory.Model, Theory |
| 2 (Type/Class) | Theory.Model, Theory |
| subtermIntruderRules | Theory.Tools.IntruderRules |
| Summary | Theory.Tools.AbstractInterpretation |
| SuperfluousLearn | Theory.Constraint.Solver.Contradictions |
| svMap | Theory.Model, Theory |
| symbol | |
| 1 (Function) | Theory.Text.Pretty |
| 2 (Function) | Theory.Text.Parser.Token |
| symbol_ | Theory.Text.Parser.Token |
| symEncMaudeSig | Theory.Model, Theory |
| System | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| SystemTraceQuantifier | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| Term | Theory.Model, Theory |
| termVar | Theory.Model, Theory |
| termVar' | Theory.Model, Theory |
| TermView | Theory.Model, Theory |
| TermView2 | Theory.Model, Theory |
| text | Theory.Text.Pretty |
| TextItem | Theory |
| TF | Theory.Model.Formula, Theory.Model, Theory |
| Theory | |
| 1 (Type/Class) | Theory |
| 2 (Data Constructor) | Theory |
| theoryAxioms | Theory |
| TheoryItem | Theory |
| theoryLemmas | Theory |
| theoryRules | Theory |
| thyCache | Theory |
| thyItems | Theory |
| thyName | Theory |
| thySignature | Theory |
| tmpdir | Theory.Tools.RuleVariants |
| toSignaturePure | Theory.Model.Signature, Theory.Model, Theory |
| toSignatureWithMaude | Theory.Model.Signature, Theory.Model, Theory |
| TraceFound | Theory.Proof, Theory |
| TraceQuantifier | Theory |
| Tracing | Theory.Tools.AbstractInterpretation |
| traverseTerm | Theory.Model, Theory |
| tryProver | Theory.Proof, Theory |
| TypedCaseDist | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| TypingLemma | Theory |
| Unchanged | Theory.Constraint.Solver.Reduction |
| UndeterminedProof | Theory.Proof, Theory |
| unifiableLNFacts | Theory.Model.Fact, Theory.Model, Theory |
| unifiableLNTerms | Theory.Model, Theory |
| unifiableRuleACInsts | Theory.Model.Rule, Theory.Model, Theory |
| unifyLNFactEqs | Theory.Model.Fact, Theory.Model, Theory |
| unifyLNTerm | Theory.Model, Theory |
| unifyLNTermFactored | Theory.Model, Theory |
| unifyLTerm | Theory.Model, Theory |
| unifyLTermFactored | Theory.Model, Theory |
| unifyRuleACInstEqs | Theory.Model.Rule, Theory.Model, Theory |
| Union | Theory.Model, Theory |
| unionSymString | Theory.Model, Theory |
| unproven | Theory.Proof, Theory |
| unprovenLemma | Theory |
| unsafefApp | Theory.Model, Theory |
| unsolvedActionAtoms | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| unsolvedChainConstraints | Theory.Constraint.Solver.CaseDistinctions, Theory.Constraint.Solver, Theory.Proof, Theory |
| unsolvedChains | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| unSplitId | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| UntypedCaseDist | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| UpK | Theory.Model.Fact, Theory.Model, Theory |
| useAutoLoopBreakersAC | Theory.Tools.LoopBreakers |
| Useful | Theory.Constraint.Solver.Goals |
| UsefulGoalNrRanking | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| Usefulness | Theory.Constraint.Solver.Goals |
| useHeuristic | Theory.Constraint.Solver.ProofMethod, Theory.Constraint.Solver, Theory.Proof, Theory |
| UseInduction | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| Var | Theory.Model, Theory |
| variantsProtoRule | Theory.Tools.RuleVariants |
| varOccurences | Theory.Model, Theory |
| varsRange | Theory.Model, Theory |
| varsRangeVFresh | Theory.Model, Theory |
| varsVTerm | Theory.Model, Theory |
| varTerm | Theory.Model, Theory |
| vcat | Theory.Text.Pretty |
| viewTerm | Theory.Model, Theory |
| viewTerm2 | Theory.Model, Theory |
| vsep | Theory.Text.Pretty |
| VTerm | Theory.Model, Theory |
| WfErrorReport | Theory.Tools.Wellformedness |
| whenChanged | Theory.Constraint.Solver.Reduction |
| whileChanging | Theory.Constraint.Solver.Reduction |
| WithMaude | Theory.Model, Theory |
| zeroWidthText | Theory.Text.Pretty |
| ZigZagMode | Theory.Text.Pretty |
| _axFormula | Theory |
| _axName | Theory |
| _cdCases | Theory.Constraint.Solver.Types |
| _cdGoal | Theory.Constraint.Solver.Types |
| _cprRuleAC | Theory |
| _cprRuleE | Theory |
| _crcInjectiveFactInsts | Theory |
| _crConstruct | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _crcRules | Theory |
| _crcTypedCaseDists | Theory |
| _crcUntypedCaseDists | Theory |
| _crDestruct | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _crProtocol | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _eqsConj | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _eqsNextSplitId | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _eqsSubst | Theory.Tools.EquationStore, Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _gsLoopBreaker | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _gsNr | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _gsSolved | Theory.Constraint.System, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcCaseDistKind | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcCaseDists | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcInjectiveFactInsts | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcRules | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcSignature | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcTraceQuantifier | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _pcUseInduction | Theory.Constraint.Solver.Types, Theory.Constraint.Solver, Theory.Proof, Theory |
| _praciLoopBreakers | Theory.Model.Rule, Theory.Model, Theory |
| _praciName | Theory.Model.Rule, Theory.Model, Theory |
| _pracLoopBreakers | Theory.Model.Rule, Theory.Model, Theory |
| _pracName | Theory.Model.Rule, Theory.Model, Theory |
| _pracVariants | Theory.Model.Rule, Theory.Model, Theory |
| _rActs | Theory.Model.Rule, Theory.Model, Theory |
| _rConcs | Theory.Model.Rule, Theory.Model, Theory |
| _rInfo | Theory.Model.Rule, Theory.Model, Theory |
| _rPrems | Theory.Model.Rule, Theory.Model, Theory |
| _sigMaudeInfo | Theory.Model.Signature, Theory.Model, Theory |
| _thyCache | Theory |
| _thyItems | Theory |
| _thyName | Theory |
| _thySignature | Theory |