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

Index

ActionCopilot.Theorem.Prove
AdmitCopilot.Theorem.Prove
admitCopilot.Theorem
altErgoCopilot.Theorem.Prover.SMT
askProverCopilot.Theorem.Prove
AssumeCopilot.Theorem.Prove
assumeCopilot.Theorem
BackendCopilot.Theorem.Prover.SMT
bmcMaxCopilot.Theorem.Kind2.Prover, Copilot.Theorem.Kind2
BoolCopilot.Theorem.Kind2
CheckCopilot.Theorem.Prove
checkCopilot.Theorem.Prove
closeProverCopilot.Theorem.Prove
combineCopilot.Theorem.Prove
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.Prover.SMT
ErrorCopilot.Theorem.Prove
ExistentialCopilot.Theorem.Prove, Copilot.Theorem
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
InitCopilot.Theorem.Kind2
InlinedCopilot.Theorem.Kind2
instantiateCopilot.Theorem
IntCopilot.Theorem.Kind2
InvalidCopilot.Theorem.Prove
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
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
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
proveCopilot.Theorem.Prove
Prover 
1 (Type/Class)Copilot.Theorem.Prove
2 (Data Constructor)Copilot.Theorem.Prove
proverNameCopilot.Theorem.Prove
RealCopilot.Theorem.Kind2
SatCopilot.Theorem.Prove
SmtFormatCopilot.Theorem.Prover.SMT
SmtLibCopilot.Theorem.Prover.SMT
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
StyleCopilot.Theorem.Kind2
TermCopilot.Theorem.Kind2
toKind2Copilot.Theorem.Kind2
TptpCopilot.Theorem.Prover.SMT
TransCopilot.Theorem.Kind2
TypeCopilot.Theorem.Kind2
UniversalCopilot.Theorem.Prove, Copilot.Theorem
UnknownCopilot.Theorem.Prove
UProofCopilot.Theorem.Prove
ValidCopilot.Theorem.Prove
ValueLiteralCopilot.Theorem.Kind2
varFlagsCopilot.Theorem.Kind2
varIdCopilot.Theorem.Kind2
varTypeCopilot.Theorem.Kind2
yicesCopilot.Theorem.Prover.SMT
z3Copilot.Theorem.Prover.SMT