Encoding

Statistics

Metric	Count
Definitions `Encoding`, `decode`, `encode`, `Γ`, `FinEncoding`, `toEncoding`, `ΓFin`, `decodeBool`, `decodeNat`, `decodeNum`, `decodePosNum`, `encodeBool`, `encodeNat`, `encodeNum`, `encodePosNum`, `encodingNatBool`, `encodingNatΓ'`, `finEncodingBoolBool`, `finEncodingNatBool`, `finEncodingNatΓ'`, `inclusionBoolΓ'`, `inhabitedEncoding`, `inhabitedFinEncoding`, `inhabitedΓ'`, `instDecidableEqΓ'`, `decEq`, `instFintypeΓ'`, `sectionΓ'Bool`, `unaryDecodeNat`, `unaryEncodeNat`, `unaryFinEncodingNat`, `Γ'`, `fintype`	33
Theorems `card_le_aleph0`, `card_le_card_list`, `decode_encode`, `encode_injective`, `card_le_aleph0`, `decode_encodeBool`, `decode_encodeNat`, `decode_encodeNum`, `decode_encodePosNum`, `encodePosNum_nonempty`, `inclusionBoolΓ'_injective`, `sectionΓ'Bool_inclusionBoolΓ'`, `unary_decode_encode_nat`	13
Total	46

Name	Category	Theorems
`Encoding` 📖	CompData	—
`FinEncoding` 📖	CompData	—
`decodeBool` 📖	CompOp	1 math math: `decode_encodeBool`
`decodeNat` 📖	CompOp	1 math math: `decode_encodeNat`
`decodeNum` 📖	CompOp	1 math math: `decode_encodeNum`
`decodePosNum` 📖	CompOp	1 math math: `decode_encodePosNum`
`encodeBool` 📖	CompOp	1 math math: `decode_encodeBool`
`encodeNat` 📖	CompOp	1 math math: `decode_encodeNat`
`encodeNum` 📖	CompOp	1 math math: `decode_encodeNum`
`encodePosNum` 📖	CompOp	1 math math: `decode_encodePosNum`
`encodingNatBool` 📖	CompOp	—
`encodingNatΓ'` 📖	CompOp	—
`finEncodingBoolBool` 📖	CompOp	—
`finEncodingNatBool` 📖	CompOp	—
`finEncodingNatΓ'` 📖	CompOp	—
`inclusionBoolΓ'` 📖	CompOp	2 math math: `sectionΓ'Bool_inclusionBoolΓ'`, `inclusionBoolΓ'_injective`
`inhabitedEncoding` 📖	CompOp	—
`inhabitedFinEncoding` 📖	CompOp	—
`inhabitedΓ'` 📖	CompOp	—
`instDecidableEqΓ'` 📖	CompOp	—
`instFintypeΓ'` 📖	CompOp	—
`sectionΓ'Bool` 📖	CompOp	1 math math: `sectionΓ'Bool_inclusionBoolΓ'`
`unaryDecodeNat` 📖	CompOp	1 math math: `unary_decode_encode_nat`
`unaryEncodeNat` 📖	CompOp	1 math math: `unary_decode_encode_nat`
`unaryFinEncodingNat` 📖	CompOp	—
`Γ'` 📖	CompData	1 math math: `inclusionBoolΓ'_injective`

Name	Kind	Assumes	Proves	Validates	Depends On
`decode_encodeBool` 📖	mathematical	—	`decodeBool` `encodeBool`	—	—
`decode_encodeNat` 📖	mathematical	—	`decodeNat` `encodeNat`	—	`Num.to_of_nat` `decode_encodeNum`
`decode_encodeNum` 📖	mathematical	—	`decodeNum` `encodeNum`	—	`decode_encodePosNum` `PosNum.cast_to_num` `encodePosNum_nonempty`
`decode_encodePosNum` 📖	mathematical	—	`decodePosNum` `encodePosNum`	—	`encodePosNum.eq_def` `decodePosNum.eq_def` `encodePosNum_nonempty`
`encodePosNum_nonempty` 📖	—	—	—	—	—
`inclusionBoolΓ'_injective` 📖	mathematical	—	`Γ'` `inclusionBoolΓ'`	—	`sectionΓ'Bool_inclusionBoolΓ'`
`sectionΓ'Bool_inclusionBoolΓ'` 📖	mathematical	—	`sectionΓ'Bool` `inclusionBoolΓ'`	—	—
`unary_decode_encode_nat` 📖	mathematical	—	`unaryDecodeNat` `unaryEncodeNat`	—	—

Name	Category	Theorems
`decode` 📖	CompOp	3 math math: `FirstOrder.Language.BoundedFormula.encoding_decode`, `FirstOrder.Language.Term.encoding_decode`, `decode_encode`
`encode` 📖	CompOp	4 math math: `encode_injective`, `FirstOrder.Language.BoundedFormula.encoding_encode`, `decode_encode`, `FirstOrder.Language.Term.encoding_encode`
`Γ` 📖	CompOp	4 math math: `card_le_card_list`, `encode_injective`, `FirstOrder.Language.Term.encoding_Γ`, `FirstOrder.Language.BoundedFormula.encoding_Γ`

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_aleph0` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.aleph0`	—	`Cardinal.mk_le_aleph0` `Function.Injective.countable` `List.countable` `encode_injective`
`card_le_card_list` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Γ`	—	`Cardinal.lift_mk_le'` `encode_injective`
`decode_encode` 📖	mathematical	—	`decode` `encode`	—	—
`encode_injective` 📖	mathematical	—	`Γ` `encode`	—	`Option.some_injective` `decode_encode`

Name	Category	Theorems
`toEncoding` 📖	CompOp	—
`ΓFin` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_aleph0` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.aleph0`	—	`Computability.Encoding.card_le_aleph0` `Finite.to_countable` `Finite.of_fintype`

Name	Category	Theorems
`decEq` 📖	CompOp	—

Name	Category	Theorems
`fintype` 📖	CompOp	—

---