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

Index

AbsoluteOffsetCopilot.Theorem.What4
ActionCopilot.Theorem.Prove
AdmitCopilot.Theorem.Prove
admitCopilot.Theorem
altErgoCopilot.Theorem.Prover.SMT
askProverCopilot.Theorem.Prove
AssumeCopilot.Theorem.Prove
assumeCopilot.Theorem
assumptionsCopilot.Theorem.What4
BackendCopilot.Theorem.Prover.SMT
baseCasesCopilot.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
bmcMaxCopilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2
BoolCopilot.Theorem.Kind2
CheckCopilot.Theorem.Prove
checkCopilot.Theorem.Prove
closeProverCopilot.Theorem.Prove
combineCopilot.Theorem.Prove
computeBisimulationProofBundleCopilot.Theorem.What4
concreteExternValuesCopilot.Theorem.What4
concreteStreamValuesCopilot.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
CVC4Copilot.Theorem.What4
cvc4Copilot.Theorem.Prover.SMT
debugCopilot.Theorem.Prover.SMT
defCopilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2
DefaultCopilot.Theorem.Prover.SMT, Copilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2
DRealCopilot.Theorem.What4
dRealCopilot.Theorem.Prover.SMT
ErrorCopilot.Theorem.Prove
ExistentialCopilot.Theorem.Prove, Copilot.Theorem
externalInputsCopilot.Theorem.What4
FConstCopilot.Theorem.Kind2
File 
1 (Type/Class)Copilot.Theorem.Kind2
2 (Data Constructor)Copilot.Theorem.Kind2
filePredsCopilot.Theorem.Kind2
filePropsCopilot.Theorem.Kind2
FunAppCopilot.Theorem.Kind2
inductionCopilot.Theorem.Prover.SMT
inductionStepCopilot.Theorem.What4
InitCopilot.Theorem.Kind2
initialStreamStateCopilot.Theorem.What4
InlinedCopilot.Theorem.Kind2
instantiateCopilot.Theorem
IntCopilot.Theorem.Kind2
Invalid 
1 (Data Constructor)Copilot.Theorem.Prove
2 (Data Constructor)Copilot.Theorem.What4
InvalidCexCopilot.Theorem.What4
kind2ProverCopilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2
kInductionCopilot.Theorem.Prover.SMT
mathsatCopilot.Theorem.Prover.SMT
maxKCopilot.Theorem.Prover.SMT
metitCopilot.Theorem.Prover.SMT
ModularCopilot.Theorem.Kind2
onlySatCopilot.Theorem.Prover.SMT
onlyValidityCopilot.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
postStreamStateCopilot.Theorem.What4
PredAppCopilot.Theorem.Kind2
PredDef 
1 (Type/Class)Copilot.Theorem.Kind2
2 (Data Constructor)Copilot.Theorem.Kind2
predIdCopilot.Theorem.Kind2
predInitCopilot.Theorem.Kind2
predStateVarsCopilot.Theorem.Kind2
predTransCopilot.Theorem.Kind2
PredTypeCopilot.Theorem.Kind2
preStreamStateCopilot.Theorem.What4
prettyPrintCopilot.Theorem.Kind2
PrimedStateVarCopilot.Theorem.Kind2
Proof 
1 (Data Constructor)Copilot.Theorem.Prove
2 (Type/Class)Copilot.Theorem.Prove, Copilot.Theorem
ProofSchemeCopilot.Theorem.Prove
Prop 
1 (Type/Class)Copilot.Theorem.Kind2
2 (Data Constructor)Copilot.Theorem.Kind2
PropIdCopilot.Theorem.Prove, Copilot.Theorem
propNameCopilot.Theorem.Kind2
PropRef 
1 (Type/Class)Copilot.Theorem.Prove, Copilot.Theorem
2 (Data Constructor)Copilot.Theorem.Prove
propTermCopilot.Theorem.Kind2
prove 
1 (Function)Copilot.Theorem.Prove
2 (Function)Copilot.Theorem.What4
ProveExceptionCopilot.Theorem.What4
Prover 
1 (Type/Class)Copilot.Theorem.Prove
2 (Data Constructor)Copilot.Theorem.Prove
proverNameCopilot.Theorem.Prove
proveWithCounterExampleCopilot.Theorem.What4
RealCopilot.Theorem.Kind2
RelativeOffsetCopilot.Theorem.What4
SatCopilot.Theorem.Prove
SatResultCopilot.Theorem.What4
SatResultCexCopilot.Theorem.What4
sideCondsCopilot.Theorem.What4
SmtFormatCopilot.Theorem.Prover.SMT
SmtLibCopilot.Theorem.Prover.SMT
SolverCopilot.Theorem.What4
startKCopilot.Theorem.Prover.SMT
startProverCopilot.Theorem.Prove
StateVarCopilot.Theorem.Kind2
StateVarDef 
1 (Type/Class)Copilot.Theorem.Kind2
2 (Data Constructor)Copilot.Theorem.Kind2
StateVarFlagCopilot.Theorem.Kind2
StatusCopilot.Theorem.Prove
StreamOffsetCopilot.Theorem.What4
streamStateCopilot.Theorem.What4
StyleCopilot.Theorem.Kind2
TermCopilot.Theorem.Kind2
toKind2Copilot.Theorem.Kind2
TptpCopilot.Theorem.Prover.SMT
TransCopilot.Theorem.Kind2
triggerStateCopilot.Theorem.What4
TypeCopilot.Theorem.Kind2
UnexpectedExistentialPropositionCopilot.Theorem.What4
UniversalCopilot.Theorem.Prove, Copilot.Theorem
Unknown 
1 (Data Constructor)Copilot.Theorem.Prove
2 (Data Constructor)Copilot.Theorem.What4
UnknownCexCopilot.Theorem.What4
UProofCopilot.Theorem.Prove
Valid 
1 (Data Constructor)Copilot.Theorem.Prove
2 (Data Constructor)Copilot.Theorem.What4
ValidCexCopilot.Theorem.What4
ValueLiteralCopilot.Theorem.Kind2
varFlagsCopilot.Theorem.Kind2
varIdCopilot.Theorem.Kind2
varTypeCopilot.Theorem.Kind2
XArrayCopilot.Theorem.What4
XBoolCopilot.Theorem.What4
XDoubleCopilot.Theorem.What4
XEmptyArrayCopilot.Theorem.What4
XExprCopilot.Theorem.What4
XFloatCopilot.Theorem.What4
XInt16Copilot.Theorem.What4
XInt32Copilot.Theorem.What4
XInt64Copilot.Theorem.What4
XInt8Copilot.Theorem.What4
XStructCopilot.Theorem.What4
XWord16Copilot.Theorem.What4
XWord32Copilot.Theorem.What4
XWord64Copilot.Theorem.What4
XWord8Copilot.Theorem.What4
YicesCopilot.Theorem.What4
yicesCopilot.Theorem.Prover.SMT
Z3Copilot.Theorem.What4
z3Copilot.Theorem.Prover.SMT