PartrecCode

📁 Source: Mathlib/Computability/PartrecCode.lean

Statistics

Metric	Count
Definitions Code, const, curry, encodeCode, eval, evaln, id, instDenumerable, instInhabited, instMembershipPFun, ofNatCode	11
Theorems computable_recOn, const_inj, curry_inj, encodeCode_eq, encode_lt_comp, encode_lt_pair, encode_lt_prec, encode_lt_rfind', eval_const, eval_curry, eval_eq_rfindOpt, eval_id, eval_part, eval_prec_succ, eval_prec_zero, evaln_bound, evaln_complete, evaln_mono, evaln_sound, exists_code, fixed_point, fixed_point₂, instCountableSubtypeForallComputable, instCountableSubtypePFunPartrec, ofNatCode_eq, primrec_const, primrec_evaln, primrec_recOn, primrec_recOn', primrec_rfind', primrec₂_comp, primrec₂_curry, primrec₂_pair, primrec₂_prec, smn, rfind'	36
Total	47

Nat.Partrec

Definitions

Name	Category	Theorems
Code 📖	CompData	20 math math: Code.encode_lt_comp, Code.primrec_pappAck_step, Code.primrec_pappAck, Code.primrec₂_comp, Code.encodeCode_eq, ComputablePred.halting_problem_not_re, Code.primrec_evaln, Code.primrec_rfind', Code.primrec₂_pair, Code.primrec₂_curry, ComputablePred.halting_problem, Code.eval_part, Code.ofNatCode_eq, Code.encode_lt_rfind', Code.encode_lt_pair, ComputablePred.halting_problem_re, Code.smn, Code.encode_lt_prec, Code.primrec_const, Code.primrec₂_prec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rfind' 📖	mathematical	—	Nat.unpaired Part Part.map Nat.rfind Part.instMonad Nat.pair	—	Partrec₂.unpaired' Partrec.map Partrec.comp Partrec.nat_iff Primrec.to_comp Primrec₂.comp Primrec₂.pair Primrec.comp Primrec.fst Primrec.unpair Primrec.nat_add Primrec.snd Nat.unpair_pair Computable.to₂

Nat.Partrec.Code

Definitions

Name	Category	Theorems
const 📖	CompOp	2 math math: eval_const, primrec_const
curry 📖	CompOp	2 math math: primrec₂_curry, eval_curry
encodeCode 📖	CompOp	1 math math: encodeCode_eq
eval 📖	CompOp	19 math math: fixed_point₂, eval_const, eval_pappAck_step_zero, fixed_point, ComputablePred.halting_problem_not_re, eval_prec_succ, eval_pappAck_step_succ, eval_id, ComputablePred.halting_problem, eval_part, ComputablePred.halting_problem_re, smn, eval_eq_rfindOpt, eval_prec_zero, exists_code, evaln_sound, evaln_complete, eval_curry, eval_pappAck
evaln 📖	CompOp	3 math math: primrec_evaln, eval_eq_rfindOpt, evaln_complete
id 📖	CompOp	1 math math: eval_id
instDenumerable 📖	CompOp	21 math math: encode_lt_comp, primrec_pappAck_step, primrec_pappAck, primrec₂_comp, ComputablePred.rice₂, encodeCode_eq, ComputablePred.halting_problem_not_re, primrec_evaln, primrec_rfind', primrec₂_pair, primrec₂_curry, ComputablePred.halting_problem, eval_part, ofNatCode_eq, encode_lt_rfind', encode_lt_pair, ComputablePred.halting_problem_re, smn, encode_lt_prec, primrec_const, primrec₂_prec
instInhabited 📖	CompOp	—
instMembershipPFun 📖	CompOp	—
ofNatCode 📖	CompOp	1 math math: ofNatCode_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
computable_recOn 📖	mathematical	Computable Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable Computable₂ Primcodable.prod	Part.bind Part.ofOption Encodable.decode Primcodable.toEncodable Part.map Encodable.encode PFun.lift	—	Computable.option_bind Computable₂.comp Computable.list_getElem? Computable.comp Computable.snd Computable.fst Computable.unpair Computable.option_map Computable.cond Computable.nat_bodd Computable.nat_div2 Computable.pair Computable.ofNat Computable.list_length Computable.option_some_iff Computable.of_eq Computable.to₂ zero_add Nat.div2_val lt_of_le_of_lt le_trans Nat.unpair_left_le Nat.unpair_right_le Option.bind_congr' ofNatCode.eq_5 Computable.id Computable.encode_iff Denumerable.ofNat_encode
const_inj 📖	—	const	—	—	—
curry_inj 📖	—	curry	—	—	—
encodeCode_eq 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable encodeCode	—	—
encode_lt_comp 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable comp	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le LinearOrderedCommMonoidWithZero.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.instAtLeastTwoHAddOfNat Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd lt_trans encode_lt_pair
encode_lt_pair 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable pair	—	lt_of_le_of_lt mul_assoc one_mul lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.left_le_pair Nat.right_le_pair
encode_lt_prec 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instZeroLEOneClass lt_trans encode_lt_pair
encode_lt_rfind' 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable rfind'	—	—
eval_const 📖	mathematical	—	eval const Part.some	—	Part.bind_some
eval_curry 📖	mathematical	—	eval curry Nat.pair	—	eval_const Part.map_some eval_id Part.bind_some
eval_eq_rfindOpt 📖	mathematical	—	eval Nat.rfindOpt evaln	—	Part.ext evaln_complete Nat.rfindOpt_mono evaln_mono
eval_id 📖	mathematical	—	eval id Part.some	—	Part.map_some Part.bind_some Nat.pair_unpair
eval_part 📖	mathematical	—	Partrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable Denumerable.nat eval	—	Partrec.of_eq Partrec.rfindOpt Computable.to₂ Computable.comp Primrec.to_comp primrec_evaln Computable.pair Computable.snd Computable.fst eval_eq_rfindOpt
eval_prec_succ 📖	mathematical	—	eval Nat.pair Part Part.instMonad	—	eval.eq_7 Nat.unpaired.eq_1 Part.bind_eq_bind Nat.unpair_pair
eval_prec_zero 📖	mathematical	—	eval Nat.pair	—	eval.eq_7 Nat.unpaired.eq_1 Nat.unpair_pair Nat.rec_zero
evaln_bound 📖	—	evaln	—	—	evaln.eq_1 evaln.eq_2 evaln.eq_3 evaln.eq_4 evaln.eq_5 evaln.eq_6 evaln.eq_7 evaln.eq_8 evaln.eq_9
evaln_complete 📖	mathematical	—	Part Part.instMembership eval evaln	—	evaln.eq_2 le_rfl evaln.eq_3 evaln.eq_4 evaln.eq_5 evaln.eq_6 Option.bind_congr' Part.bind_map le_max_of_le_left evaln_bound evaln_mono le_max_left le_max_right evaln.eq_7 evaln.eq_8 le_trans Nat.unpair_pair evaln.eq_9 Nat.pair_unpair zero_add instIsEmptyFalse add_comm add_left_comm evaln_sound
evaln_mono 📖	—	evaln	—	—	evaln.eq_1 le_trans evaln.eq_2 evaln.eq_3 evaln.eq_4 evaln.eq_5 evaln.eq_6 Option.bind_congr' evaln.eq_7 evaln.eq_8 evaln.eq_9 Nat.pair_unpair
evaln_sound 📖	mathematical	evaln	Part Part.instMembership eval	—	evaln.eq_1 evaln.eq_2 evaln.eq_3 evaln.eq_4 evaln.eq_5 Part.bind_map evaln.eq_6 Option.bind_congr' evaln.eq_7 evaln.eq_8 evaln_mono Nat.unpair_pair evaln.eq_9 Nat.pair_unpair zero_add add_comm add_left_comm
exists_code 📖	mathematical	—	eval	—	eval_id Part.map_some Part.bind_some Nat.unpair_pair add_zero Part.map_id' Nat.Partrec.rfind'
fixed_point 📖	mathematical	Computable Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable	eval	—	Partrec.bind Partrec₂.comp eval_part Computable.comp Computable.ofNat Computable.fst Partrec.to₂ Computable.snd exists_code Denumerable.decode_eq_ofNat Denumerable.ofEquiv_ofNat Denumerable.sigma_ofNat_val Nat.unpair_pair Part.bind_some Primrec.to_comp Primrec₂.comp primrec₂_curry Primrec.const Primrec.id Part.map_some eval_curry Denumerable.ofNat_encode Part.map_id'
fixed_point₂ 📖	mathematical	Partrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable Denumerable.nat	eval	—	exists_code eval_curry Denumerable.decode_eq_ofNat Denumerable.ofEquiv_ofNat Denumerable.sigma_ofNat_val Nat.unpair_pair Denumerable.ofNat_encode Part.map_id' Part.bind_some fixed_point Primrec.to_comp Primrec₂.comp primrec₂_curry Primrec.const Primrec.encode
instCountableSubtypeForallComputable 📖	mathematical	—	Countable Computable Primcodable.ofDenumerable Denumerable.nat	—	Function.Injective.countable PFun.lift_injective
instCountableSubtypePFunPartrec 📖	mathematical	—	Countable PFun Primcodable.ofDenumerable Denumerable.nat	—	Function.Surjective.countable Encodable.countable Partrec₂.comp eval_part Computable.const Computable.id Part.bind_some exists_code
ofNatCode_eq 📖	mathematical	—	Denumerable.ofNat Nat.Partrec.Code instDenumerable ofNatCode	—	—
primrec_const 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable const Encodable.decode Denumerable.nat	—	Primrec.of_eq Primrec.nat_iterate Primrec.id Primrec.const Primrec.to₂ Primrec₂.comp primrec₂_comp Primrec.snd Function.iterate_succ'
primrec_evaln 📖	mathematical	—	Encodable.encode Option.encodable Primcodable.toEncodable Primcodable.option Primcodable.ofDenumerable Denumerable.nat Nat.Partrec.Code evaln Encodable.decode Primcodable.prod instDenumerable	—	Primrec.to₂ Primrec.comp Primrec.snd Denumerable.prod_ofNat_val Nat.pair_unpair Denumerable.encode_ofNat evaln.eq_1 Option.bind_congr' Nat.unpair_pair Denumerable.ofNat_encode evaln.eq_2 guard.congr_simp guard_true evaln.eq_3 evaln.eq_4 evaln.eq_5 evaln.eq_6 encode_lt_pair Nat.pair_lt_pair_right evaln.eq_7 encode_lt_comp evaln.eq_8 Nat.pair_lt_pair_left evaln.eq_9 encode_lt_rfind' Primrec.of_eq Primrec.option_bind Primrec₂.comp Primrec.list_getElem? Primrec.const Primrec.encode_iff Primrec.fst Denumerable.ofEquiv_ofNat Denumerable.sigma_ofNat_val
primrec_recOn 📖	—	Encodable.encode Nat.Partrec.Code Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable Encodable.decode Primcodable.prod	—	—	primrec_recOn'
primrec_recOn' 📖	—	Encodable.encode Nat.Partrec.Code Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable Encodable.decode Primrec₂ Primcodable.prod	—	—	Primrec.option_bind Primrec₂.comp Primrec.list_getElem? Primrec.comp Primrec.snd Primrec.fst Primrec.unpair Primrec.option_map Primrec.cond Primrec.nat_bodd Primrec.nat_div2 Primrec.pair Primrec.ofNat Primrec.list_length Primrec.option_some_iff Primrec.of_eq Primrec.to₂ zero_add Nat.div2_val lt_of_le_of_lt le_trans Nat.unpair_left_le Nat.unpair_right_le Option.bind_congr' ofNatCode.eq_5 Primrec.id Primrec.encode_iff Denumerable.ofNat_encode
primrec_rfind' 📖	mathematical	—	Encodable.encode Nat.Partrec.Code Option.encodable Primcodable.toEncodable Primcodable.ofDenumerable instDenumerable rfind' Encodable.decode	—	Primrec.ofNat_iff Primrec.encode_iff Primrec₂.comp Primrec.nat_add Primrec.comp Primrec.nat_double_succ Primrec.ofNat Primrec.const
primrec₂_comp 📖	mathematical	—	Primrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable comp	—	Primrec₂.ofNat_iff Primrec₂.encode_iff Primrec₂.comp Primrec.nat_add Primrec.comp Primrec.nat_double Primrec.nat_double_succ Primrec₂.natPair Primrec.encode_iff Primrec.ofNat Primrec.fst Primrec.snd Primrec₂.const
primrec₂_curry 📖	mathematical	—	Primrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable Denumerable.nat curry	—	Primrec₂.comp primrec₂_comp Primrec.fst primrec₂_pair Primrec.comp primrec_const Primrec.snd Primrec.const
primrec₂_pair 📖	mathematical	—	Primrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable pair	—	Primrec₂.ofNat_iff Primrec₂.encode_iff Primrec₂.comp Primrec.nat_add Primrec.comp Primrec.nat_double Primrec₂.natPair Primrec.encode_iff Primrec.ofNat Primrec.fst Primrec.snd Primrec₂.const
primrec₂_prec 📖	mathematical	—	Primrec₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable	—	Primrec₂.ofNat_iff Primrec₂.encode_iff Primrec₂.comp Primrec.nat_add Primrec.comp Primrec.nat_double_succ Primrec.nat_double Primrec₂.natPair Primrec.encode_iff Primrec.ofNat Primrec.fst Primrec.snd Primrec₂.const
smn 📖	mathematical	—	Computable₂ Nat.Partrec.Code Primcodable.ofDenumerable instDenumerable Denumerable.nat eval Nat.pair	—	Primrec₂.to_comp primrec₂_curry eval_curry

---

← Back to Index