| ::: | |
| 1 (Type/Class) | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| 2 (Data Constructor) | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| A | Zsyntax.Labelled.Formula |
| act | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| ActCase | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| activate | Otter.Internal.Structures |
| Active | Otter.Internal.Structures |
| ActiveNode | Otter.Internal.Structures |
| ActiveNodes | Otter.Internal.Structures |
| addInactive | Otter.Internal.Search |
| addRule | Otter.Internal.Search |
| addToInactives | Otter.Internal.Structures |
| AllResults | Otter.SearchRes, Otter, Zsyntax |
| AnnLSequent | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| apply | Otter.Rule, Otter |
| arrowDimap | Otter.Rule, Otter |
| Atom | Zsyntax.Labelled.Formula |
| atom | Zsyntax.Formula, Zsyntax |
| axForget | Zsyntax.Formula, Zsyntax |
| Axiom | |
| 1 (Type/Class) | Zsyntax.Formula, Zsyntax |
| 2 (Data Constructor) | Zsyntax.Formula, Zsyntax |
| axiom | Zsyntax.Formula, Zsyntax |
| axiom' | Zsyntax.Formula, Zsyntax |
| axLabel | Zsyntax.Labelled.Formula |
| axToFormula | Zsyntax.Labelled.Formula |
| BAtom | Zsyntax.Labelled.Formula |
| bAtom | Zsyntax.Labelled.Formula |
| BConj | Zsyntax.Labelled.Formula |
| bConj | Zsyntax.Labelled.Formula |
| BFormula | Zsyntax.Labelled.Formula |
| bfToAtoms | Zsyntax.Labelled.Formula |
| bfToFormula | Zsyntax.Labelled.Formula |
| BioAtom | Zsyntax.Formula, Zsyntax |
| BioFormula | Zsyntax.Formula, Zsyntax |
| BioInter | Zsyntax.Formula, Zsyntax |
| BipoleRel | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| BipoleRule | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| BSChecked | Otter.Internal.Structures |
| BSCheckedNode | Otter.Internal.Structures |
| Concl | Otter.Internal.Structures |
| concl | Zsyntax.Labelled.DerivationTerm |
| ConclNode | Otter.Internal.Structures |
| Conj | Zsyntax.Labelled.Formula |
| conj | Zsyntax.Formula, Zsyntax |
| ConjL | Zsyntax.Labelled.DerivationTerm |
| ConjR | Zsyntax.Labelled.DerivationTerm |
| cons | Otter.SearchRes, Otter |
| Copy | Zsyntax.Labelled.DerivationTerm |
| copyRule | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| CS | Zsyntax.ReactionList |
| CSC | Zsyntax.ReactionList |
| CtrlSet | Zsyntax.ReactionList |
| CtrlSetCtxt | Zsyntax.ReactionList |
| CtrlType | Zsyntax.ReactionList |
| decideNeutral | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| DecoratedFormula | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| DecoratedLSequent | Zsyntax |
| deepHetComp | Zsyntax.Labelled.Formula |
| Delay | Otter.SearchRes, Otter |
| delay | Otter.SearchRes, Otter |
| DerivationTerm | Zsyntax.Labelled.DerivationTerm |
| dfLabel | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| doSearch | Otter.Internal.Search |
| DTFocMatchRes | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| DTMatchRes | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| ElemBase | |
| 1 (Type/Class) | Zsyntax.Labelled.Formula |
| 2 (Data Constructor) | Zsyntax.Labelled.Formula |
| elemBase | Zsyntax.Labelled.Formula |
| elemBaseAll | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| emptyActives | Otter.Internal.Structures |
| emptyGI | Otter.Internal.Structures |
| emptyInactives | Otter.Internal.Structures |
| EmptyXiFullResult | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| EmptyZetaXi | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| extend | Zsyntax.ReactionList |
| Extraction | Otter.SearchRes, Otter, Zsyntax |
| extractNode | Otter.Internal.Structures |
| extractResults | Otter.SearchRes, Otter, Zsyntax |
| FailureReason | Otter.SearchRes, Otter, Zsyntax |
| filterImpl | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| filterUnsubsumed | Otter.Internal.Search |
| FKind | Zsyntax.Labelled.Formula |
| foc | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| FocMatchRes | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| focus | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| foldActives | Otter.Internal.Structures |
| Formula | |
| 1 (Type/Class) | Zsyntax.Formula, Zsyntax |
| 2 (Data Constructor) | Zsyntax.Formula, Zsyntax |
| frmlHetEq | Zsyntax.Labelled.Formula |
| frmlHetOrd | Zsyntax.Labelled.Formula |
| frNeg | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| fromCSCtxts | Zsyntax.ReactionList |
| frontier | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| frPos | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| FSChecked | Otter.Internal.Structures |
| FSCheckedNode | Otter.Internal.Structures |
| FullXiEmptyResult | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| FullZetaXi | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| fwdSubsumes | Otter.Internal.Structures |
| generateRule | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| getActives | Otter.Internal.Search |
| getRules | Otter.Internal.Search |
| GlIndex | Otter.Internal.Structures |
| GlobalIndex | Otter.Internal.Structures |
| GNS | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| Goal | Otter.Internal.Structures |
| GoalNSequent | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| haveGoal | Otter.Internal.Search |
| Impl | Zsyntax.Labelled.Formula |
| impl | Zsyntax.Formula, Zsyntax |
| ImplL | Zsyntax.Labelled.DerivationTerm |
| implLeft | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| ImplR | Zsyntax.Labelled.DerivationTerm |
| implRight | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| Inactive | Otter.Internal.Structures |
| InactiveNode | Otter.Internal.Structures |
| InactiveNodes | Otter.Internal.Structures |
| Init | Zsyntax.Labelled.DerivationTerm |
| Initial | Otter.Internal.Structures |
| initialize | Otter.Internal.Structures |
| initialRules | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| initIsBSCheckd | Otter.Internal.Structures |
| initIsFSCheckd | Otter.Internal.Structures |
| IsFocusable | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| isGoalM | Otter.Internal.Search |
| isNotFwdSubsumed | Otter.Internal.Search |
| justCS | Zsyntax.ReactionList |
| KAtom | Zsyntax.Labelled.Formula |
| KConj | Zsyntax.Labelled.Formula |
| KImpl | Zsyntax.Labelled.Formula |
| L | Zsyntax.Labelled.Formula |
| Label | |
| 1 (Type/Class) | Zsyntax.Labelled.Formula |
| 2 (Type/Class) | Zsyntax |
| label | Zsyntax.Labelled.Formula |
| LAx | Zsyntax.Labelled.Formula |
| LAxiom | Zsyntax.Labelled.Formula |
| lcBase | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| LCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| leftActive | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| LFormula | Zsyntax.Labelled.Formula |
| LinNeg | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| LinPos | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| loop | Otter.Internal.Search |
| LS | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| lsConcl | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| lsCty | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| LSequent | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| lsLCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| lsUCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| lToS | Zsyntax.Formula, Zsyntax |
| match | Otter.Rule, Otter |
| matchLinearCtxt | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| matchMultiSet | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| matchRel | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| MatchRes | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| matchSchema | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| maybeBFormula | Zsyntax.Labelled.Formula |
| maybeNeutral | Zsyntax.Formula, Zsyntax |
| mayProperRule | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| maySequent | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| merge | Otter.Internal.Search |
| mkGoal | Otter.Internal.Structures |
| MREmptyGoal | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| MRFullGoal | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| msRespectsCS | Zsyntax.ReactionList |
| N | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| Neutral | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| neutralize | Zsyntax.Formula, Zsyntax |
| neutralizeFormula | Zsyntax.Formula, Zsyntax |
| neutralizeOs | Zsyntax.Formula, Zsyntax |
| NeutralKind | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| NoResults | Otter.SearchRes, Otter, Zsyntax |
| normalize | Zsyntax.Formula, Zsyntax |
| NotATheorem | Otter.SearchRes, Otter, Zsyntax |
| nuLabel | Zsyntax.Formula, Zsyntax |
| O | Zsyntax.Labelled.Formula |
| oConj | Zsyntax.Labelled.Formula |
| oImpl | Zsyntax.Labelled.Formula |
| Opaque | Zsyntax.Labelled.Formula |
| percolate | Otter.Internal.Search |
| popInactive | Otter.Internal.Search |
| popInactiveOp | Otter.Internal.Structures |
| positiveFocalDispatch | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| ppBioFormula | Zsyntax.Formula, Zsyntax |
| ppFormula | Zsyntax.Formula, Zsyntax |
| ppLAxiom | Zsyntax.Labelled.Formula |
| ppLFormula | Zsyntax.Labelled.Formula |
| processNewActive | Otter.Internal.Search |
| ProperRule | |
| 1 (Type/Class) | Otter.Rule, Otter |
| 2 (Type/Class) | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| Prover | Otter.Internal.Search |
| ProverState | Otter.Internal.Search |
| PS | Otter.Internal.Search |
| ReactionList | Zsyntax.Labelled.Formula |
| Regular | Zsyntax.ReactionList |
| relDimap | Otter.Rule, Otter |
| removeSubsumedBy | Otter.Internal.Search |
| removeSubsumedByOp | Otter.Internal.Structures |
| Res | |
| 1 (Type/Class) | Otter.SearchRes, Otter |
| 2 (Data Constructor) | Otter.SearchRes, Otter |
| respects | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| respectsCC | Zsyntax.ReactionList |
| respectsRList | Zsyntax.ReactionList |
| RL | Zsyntax.ReactionList |
| RList | Zsyntax.ReactionList |
| Rule | |
| 1 (Type/Class) | Otter.Rule, Otter |
| 2 (Data Constructor) | Otter.Rule, Otter |
| RuleAppRes | Otter.Internal.Search |
| SC | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| SchemaLCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| search | |
| 1 (Function) | Otter.Internal.Search, Otter |
| 2 (Function) | Zsyntax |
| searchLabelled | Zsyntax |
| SearchNode | Otter.Internal.Structures |
| SearchProperRule | Otter.Internal.Structures |
| SearchRes | Otter.SearchRes, Otter, Zsyntax |
| SearchRule | Otter.Internal.Structures |
| Sequent | Zsyntax.Formula, Zsyntax |
| SLC | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| SpaceTooBig | Otter.SearchRes, Otter, Zsyntax |
| SQ | Zsyntax.Formula, Zsyntax |
| SSchema | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| SSEmptyGoal | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| SSFullGoal | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| Stage | Otter.Internal.Structures |
| SubCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| subCtxtOf | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| Subsumable | Otter.Internal.Structures, Otter |
| subsumes | Otter.Internal.Structures, Otter |
| SupersetClosed | Zsyntax.ReactionList |
| switchN | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| toCtxtList | Zsyntax.ReactionList |
| toGoalSequent | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| toLabelledGoal | Zsyntax |
| toProperRule | Otter.Internal.Structures |
| transitions | Zsyntax.Labelled.DerivationTerm |
| UCtxt | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| unCS | Zsyntax.ReactionList |
| unEB | Zsyntax.Labelled.Formula |
| Unrestr | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| unRL | Zsyntax.ReactionList |
| unRule | Otter.Rule, Otter |
| unSA | Zsyntax.Formula, Zsyntax |
| withMaybeNeutral | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| withNeutral | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| withOpaque | Zsyntax.Labelled.Formula |
| ZetaXi | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| _actives | Otter.Internal.Search |
| _cscCtxt | Zsyntax.ReactionList |
| _cscType | Zsyntax.ReactionList |
| _gnsConcl | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| _gnsLC | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| _gnsUC | Zsyntax.Labelled.Rule.Frontier, Zsyntax.Labelled.Rule |
| _inactives | Otter.Internal.Search |
| _index | Otter.Internal.Search |
| _isGoal | Otter.Internal.Search |
| _payload | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |
| _rules | Otter.Internal.Search |
| _scOnOnlyFirst | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| _scRestFirst | Zsyntax.Labelled.Rule.Interface, Zsyntax.Labelled.Rule |
| _sqConcl | Zsyntax.Formula, Zsyntax |
| _sqLC | Zsyntax.Formula, Zsyntax |
| _sqUC | Zsyntax.Formula, Zsyntax |
| _term | Zsyntax.Labelled.Rule.BipoleRelation, Zsyntax.Labelled.Rule |