copilot-theorem-4.8: k-induction for Copilot.

Index

AbsoluteOffset | Copilot.Theorem.What4
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
baseCases | Copilot.Theorem.What4
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
concreteExternValues | Copilot.Theorem.What4
concreteStreamValues | Copilot.Theorem.What4
CopilotValue |
1 (Type/Class) | Copilot.Theorem.What4
2 (Data Constructor) | Copilot.Theorem.What4
CounterExample |
1 (Type/Class) | Copilot.Theorem.What4
2 (Data Constructor) | 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
fileNodes | Copilot.Theorem.Kind2
fileProps | Copilot.Theorem.Kind2
fileTopNode | Copilot.Theorem.Kind2
FunApp | Copilot.Theorem.Kind2
induction | Copilot.Theorem.Prover.SMT
inductionStep | Copilot.Theorem.What4
Init | Copilot.Theorem.Kind2
initialStreamState | Copilot.Theorem.What4
instantiate | Copilot.Theorem
Int | Copilot.Theorem.Kind2
Invalid |
1 (Data Constructor) | Copilot.Theorem.Prove
2 (Data Constructor) | Copilot.Theorem.What4
InvalidCex | 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
Node |
1 (Type/Class) | Copilot.Theorem.Kind2
2 (Data Constructor) | Copilot.Theorem.Kind2
nodeId | Copilot.Theorem.Kind2
nodeInit | Copilot.Theorem.Kind2
nodeStateVars | Copilot.Theorem.Kind2
nodeTrans | 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
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
ProveException | Copilot.Theorem.What4
Prover |
1 (Type/Class) | Copilot.Theorem.Prove
2 (Data Constructor) | Copilot.Theorem.Prove
proverName | Copilot.Theorem.Prove
proveWithCounterExample | Copilot.Theorem.What4
Real | Copilot.Theorem.Kind2
RelativeOffset | Copilot.Theorem.What4
Sat | Copilot.Theorem.Prove
SatResult | Copilot.Theorem.What4
SatResultCex | 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
StreamOffset | Copilot.Theorem.What4
streamState | Copilot.Theorem.What4
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
UnexpectedExistentialProposition | Copilot.Theorem.What4
Universal | Copilot.Theorem.Prove, Copilot.Theorem
Unknown |
1 (Data Constructor) | Copilot.Theorem.Prove
2 (Data Constructor) | Copilot.Theorem.What4
UnknownCex | Copilot.Theorem.What4
UProof | Copilot.Theorem.Prove
Valid |
1 (Data Constructor) | Copilot.Theorem.Prove
2 (Data Constructor) | Copilot.Theorem.What4
ValidCex | 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