| Action | Copilot.Theorem.Prove |
| Admit | Copilot.Theorem.Prove |
| admit | Copilot.Theorem |
| altErgo | Copilot.Theorem.Prover.SMT |
| askProver | Copilot.Theorem.Prove |
| Assume | Copilot.Theorem.Prove |
| assume | Copilot.Theorem |
| assumptions | Copilot.Theorem.What4 |
| Backend | Copilot.Theorem.Prover.SMT |
| BisimulationProofBundle | |
| 1 (Type/Class) | Copilot.Theorem.What4 |
| 2 (Data Constructor) | Copilot.Theorem.What4 |
| BisimulationProofState | |
| 1 (Type/Class) | Copilot.Theorem.What4 |
| 2 (Data Constructor) | Copilot.Theorem.What4 |
| bmcMax | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| Bool | Copilot.Theorem.Kind2 |
| Check | Copilot.Theorem.Prove |
| check | Copilot.Theorem.Prove |
| closeProver | Copilot.Theorem.Prove |
| combine | Copilot.Theorem.Prove |
| computeBisimulationProofBundle | Copilot.Theorem.What4 |
| CVC4 | Copilot.Theorem.What4 |
| cvc4 | Copilot.Theorem.Prover.SMT |
| debug | Copilot.Theorem.Prover.SMT |
| def | Copilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| Default | Copilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| DReal | Copilot.Theorem.What4 |
| dReal | Copilot.Theorem.Prover.SMT |
| Error | Copilot.Theorem.Prove |
| Existential | Copilot.Theorem.Prove, Copilot.Theorem |
| externalInputs | Copilot.Theorem.What4 |
| FConst | Copilot.Theorem.Kind2 |
| File | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| filePreds | Copilot.Theorem.Kind2 |
| fileProps | Copilot.Theorem.Kind2 |
| FunApp | Copilot.Theorem.Kind2 |
| induction | Copilot.Theorem.Prover.SMT |
| Init | Copilot.Theorem.Kind2 |
| initialStreamState | Copilot.Theorem.What4 |
| Inlined | Copilot.Theorem.Kind2 |
| instantiate | Copilot.Theorem |
| Int | Copilot.Theorem.Kind2 |
| Invalid | |
| 1 (Data Constructor) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.What4 |
| kind2Prover | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| kInduction | Copilot.Theorem.Prover.SMT |
| mathsat | Copilot.Theorem.Prover.SMT |
| maxK | Copilot.Theorem.Prover.SMT |
| metit | Copilot.Theorem.Prover.SMT |
| Modular | Copilot.Theorem.Kind2 |
| onlySat | Copilot.Theorem.Prover.SMT |
| onlyValidity | Copilot.Theorem.Prover.SMT |
| Options | |
| 1 (Type/Class) | Copilot.Theorem.Prover.SMT |
| 2 (Data Constructor) | Copilot.Theorem.Prover.SMT |
| 3 (Type/Class) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| 4 (Data Constructor) | Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2 |
| Output | |
| 1 (Type/Class) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| postStreamState | Copilot.Theorem.What4 |
| PredApp | Copilot.Theorem.Kind2 |
| PredDef | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| predId | Copilot.Theorem.Kind2 |
| predInit | Copilot.Theorem.Kind2 |
| predStateVars | Copilot.Theorem.Kind2 |
| predTrans | Copilot.Theorem.Kind2 |
| PredType | Copilot.Theorem.Kind2 |
| preStreamState | Copilot.Theorem.What4 |
| prettyPrint | Copilot.Theorem.Kind2 |
| PrimedStateVar | Copilot.Theorem.Kind2 |
| Proof | |
| 1 (Data Constructor) | Copilot.Theorem.Prove |
| 2 (Type/Class) | Copilot.Theorem.Prove, Copilot.Theorem |
| ProofScheme | Copilot.Theorem.Prove |
| Prop | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| PropId | Copilot.Theorem.Prove, Copilot.Theorem |
| propName | Copilot.Theorem.Kind2 |
| PropRef | |
| 1 (Type/Class) | Copilot.Theorem.Prove, Copilot.Theorem |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| propTerm | Copilot.Theorem.Kind2 |
| prove | |
| 1 (Function) | Copilot.Theorem.Prove |
| 2 (Function) | Copilot.Theorem.What4 |
| Prover | |
| 1 (Type/Class) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.Prove |
| proverName | Copilot.Theorem.Prove |
| Real | Copilot.Theorem.Kind2 |
| Sat | Copilot.Theorem.Prove |
| SatResult | Copilot.Theorem.What4 |
| sideConds | Copilot.Theorem.What4 |
| SmtFormat | Copilot.Theorem.Prover.SMT |
| SmtLib | Copilot.Theorem.Prover.SMT |
| Solver | Copilot.Theorem.What4 |
| startK | Copilot.Theorem.Prover.SMT |
| startProver | Copilot.Theorem.Prove |
| StateVar | Copilot.Theorem.Kind2 |
| StateVarDef | |
| 1 (Type/Class) | Copilot.Theorem.Kind2 |
| 2 (Data Constructor) | Copilot.Theorem.Kind2 |
| StateVarFlag | Copilot.Theorem.Kind2 |
| Status | Copilot.Theorem.Prove |
| streamState | Copilot.Theorem.What4 |
| Style | Copilot.Theorem.Kind2 |
| Term | Copilot.Theorem.Kind2 |
| toKind2 | Copilot.Theorem.Kind2 |
| Tptp | Copilot.Theorem.Prover.SMT |
| Trans | Copilot.Theorem.Kind2 |
| triggerState | Copilot.Theorem.What4 |
| Type | Copilot.Theorem.Kind2 |
| Universal | Copilot.Theorem.Prove, Copilot.Theorem |
| Unknown | |
| 1 (Data Constructor) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.What4 |
| UProof | Copilot.Theorem.Prove |
| Valid | |
| 1 (Data Constructor) | Copilot.Theorem.Prove |
| 2 (Data Constructor) | Copilot.Theorem.What4 |
| ValueLiteral | Copilot.Theorem.Kind2 |
| varFlags | Copilot.Theorem.Kind2 |
| varId | Copilot.Theorem.Kind2 |
| varType | Copilot.Theorem.Kind2 |
| XArray | Copilot.Theorem.What4 |
| XBool | Copilot.Theorem.What4 |
| XDouble | Copilot.Theorem.What4 |
| XEmptyArray | Copilot.Theorem.What4 |
| XExpr | Copilot.Theorem.What4 |
| XFloat | Copilot.Theorem.What4 |
| XInt16 | Copilot.Theorem.What4 |
| XInt32 | Copilot.Theorem.What4 |
| XInt64 | Copilot.Theorem.What4 |
| XInt8 | Copilot.Theorem.What4 |
| XStruct | Copilot.Theorem.What4 |
| XWord16 | Copilot.Theorem.What4 |
| XWord32 | Copilot.Theorem.What4 |
| XWord64 | Copilot.Theorem.What4 |
| XWord8 | Copilot.Theorem.What4 |
| Yices | Copilot.Theorem.What4 |
| yices | Copilot.Theorem.Prover.SMT |
| Z3 | Copilot.Theorem.What4 |
| z3 | Copilot.Theorem.Prover.SMT |