Computable

Statistics

Metric	Count
Definitions `Computable`, `Computable`, `EvalsTo`, `EvalsToInTime`, `FinTM2`, `Cfg`, `K`, `Stmt`, `decidableEqK`, `inhabitedCfg`, `inhabitedStmt`, `inhabitedσ`, `initialState`, `kDecidableEq`, `kFin`, `k₀`, `k₁`, `m`, `main`, `step`, `Γ`, `Γk₀Fin`, `Λ`, `ΛFin`, `σ`, `σFin`, `TM2Computable`, `outputsFun`, `toTM2ComputableAux`, `TM2ComputableAux`, `inputAlphabet`, `outputAlphabet`, `tm`, `TM2ComputableInPolyTime`, `outputsFun`, `time`, `toTM2ComputableAux`, `toTM2ComputableInTime`, `TM2ComputableInTime`, `outputsFun`, `time`, `toTM2Computable`, `toTM2ComputableAux`, `TM2Outputs`, `TM2OutputsInTime`, `toTM2Outputs`, `haltList`, `idComputable`, `idComputableInPolyTime`, `idComputableInTime`, `idComputer`, `inhabitedEvalsToInTime`, `inhabitedFinTM2`, `inhabitedTM2Computable`, `inhabitedTM2ComputableAux`, `inhabitedTM2ComputableInPolyTime`, `inhabitedTM2ComputableInTime`, `inhabitedTM2EvalsTo`, `inhabitedTM2Outputs`, `inhabitedTM2OutputsInTime`, `initList`	61
Theorems	0
Total	61

Name	Category	Theorems
`Computable` 📖	MathDef	5 math math: `ULower.down_computable`, `Computable.symm`, `Computable.eqv`, `Computable.equiv₂`, `Computable.trans`

Name	Category	Theorems
`EvalsTo` 📖	CompOp	—
`EvalsToInTime` 📖	CompOp	—
`FinTM2` 📖	CompData	—
`TM2Computable` 📖	CompData	—
`TM2ComputableAux` 📖	CompData	—
`TM2ComputableInPolyTime` 📖	CompData	—
`TM2ComputableInTime` 📖	CompData	—
`TM2Outputs` 📖	CompOp	—
`TM2OutputsInTime` 📖	CompOp	—
`haltList` 📖	CompOp	—
`idComputable` 📖	CompOp	—
`idComputableInPolyTime` 📖	CompOp	—
`idComputableInTime` 📖	CompOp	—
`idComputer` 📖	CompOp	—
`inhabitedEvalsToInTime` 📖	CompOp	—
`inhabitedFinTM2` 📖	CompOp	—
`inhabitedTM2Computable` 📖	CompOp	—
`inhabitedTM2ComputableAux` 📖	CompOp	—
`inhabitedTM2ComputableInPolyTime` 📖	CompOp	—
`inhabitedTM2ComputableInTime` 📖	CompOp	—
`inhabitedTM2EvalsTo` 📖	CompOp	—
`inhabitedTM2Outputs` 📖	CompOp	—
`inhabitedTM2OutputsInTime` 📖	CompOp	—
`initList` 📖	CompOp	—

Name	Category	Theorems
`outputsFun` 📖	CompOp	—
`toTM2ComputableAux` 📖	CompOp	—

Name	Category	Theorems
`toTM2Outputs` 📖	CompOp	—

Name	Category	Theorems
`Computable` 📖	MathDef	47 math math: `Computable.of_eq`, `ComputablePred.decide`, `Computable.encode_iff`, `computablePred_iff_computable_decide`, `Computable.list_reverse`, `Computable.option_getD`, `Computable.encode`, `Computable.ofNat`, `Computable.decode`, `Primrec.to_comp`, `Computable.sumInr`, `Nat.Partrec.Code.instCountableSubtypeForallComputable`, `Computable.option_some_iff`, `Computable.snd`, `Computable.sumInl`, `Computable.vector_ofFn'`, `Computable₂.comp`, `Computable.vector_ofFn`, `Computable.unpair`, `Computable.vector_head`, `Computable.comp`, `Computable.list_length`, `Computable.nat_rec`, `Computable.option_casesOn`, `Nat.Partrec'.vec_iff`, `Computable.option_some`, `Computable.vector_toList`, `Computable.vector_length`, `ComputablePred.ite`, `Computable.pair`, `Computable.nat_casesOn`, `Computable.succ`, `Computable.option_map`, `Computable.fst`, `Computable.cond`, `Computable.nat_div2`, `Partrec.of_eq_tot`, `Computable.list_ofFn`, `Computable.const`, `ComputablePred.computable_iff`, `Computable.option_bind`, `Computable.pred`, `Computable.nat_bodd`, `Computable.vector_tail`, `Computable.id`, `Computable.sumCasesOn`, `Computable.subtype_mk`

---