Term BV term BShift le
LO.FirstOrder.Arithmetic.Bootstrapping.termBV_termBShift_le
Plain-language statement
termBShift shifts the bound-variable depth up by exactly one (on well-formed terms): so t is a level-m term iff termBShift t is level-(m+1). The ←-direction recovers the lowered arity, which is how the bounded-∀ bound (a termBShift-image) is recognized as a bShift of a real term of the outer arity.
Exact Lean statement
lemma termBV_termBShift_le {t : V} (ht : IsUTerm L t) (m : V) :
termBV L (termBShift L t) ≤ m + 1 ↔ termBV L t ≤ mFormal artifact
Lean source
lemma termBV_termBShift_le {t : V} (ht : IsUTerm L t) (m : V) : termBV L (termBShift L t) ≤ m + 1 ↔ termBV L t ≤ m := by refine IsUTerm.induction 𝚺 (P := fun t ↦ termBV L (termBShift L t) ≤ m + 1 ↔ termBV L t ≤ m) ?_ ?_ ?_ ?_ t ht · definability · intro z; simp only [termBShift_bvar, termBV_bvar]; exact add_le_add_iff_right 1 · intro x; simp only [termBShift_fvar, termBV_fvar]; exact iff_of_true zero_le zero_le · intro k f v hf hv ih rw [termBShift_func hf hv, termBV_func hf hv.termBShiftVec, termBV_func hf hv, listMaxss_le_iff, listMaxss_le_iff] constructor · intro H i hi rw [len_termBVVec hv] at hi rw [nth_termBVVec hv hi, ← ih i hi] have := H i (by rw [len_termBVVec hv.termBShiftVec]; exact hi) rwa [nth_termBVVec hv.termBShiftVec hi, nth_termBShiftVec hv hi] at this · intro H i hi rw [len_termBVVec hv.termBShiftVec] at hi rw [nth_termBVVec hv.termBShiftVec hi, nth_termBShiftVec hv hi, ih i hi] have := H i (by rw [len_termBVVec hv]; exact hi) rwa [nth_termBVVec hv hi] at this- Project
- Foundation
- License
- Apache-2.0
- Commit
- 8dcdb3196454
- Source
- Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean:521-541
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Computable Pred iff decoded pred
ComputablePred.iff_decoded_pred
Plain-language statement
Computability of a predicate on a Primcodable type is equivalent to the computability of the corresponding predicate on ℕ obtained by decoding.
Source project: Foundation
Person-level attribution pending.
Bv quote fixitr
LO.FirstOrder.Arithmetic.Bootstrapping.bv_quote_fixitr
Plain-language statement
bv-pin bridge (over ℕ): bv ⌜fixitr 0 (fvSup χ) ▹ χ⌝ = fvSup χ. - ≤ is immediate from quote_univCl_eq + bv_qqAlls (closing fvSup quantifiers reaches a sentence, whose bv is 0). - ≥ is by level-factoring: were the body an IsSemiformula j for some j < fvSup, IsSemiformula.sound + castLE-invariance would re-express χ as `γ ⇜ ![...
Source project: Foundation
Person-level attribution pending.
Conj
LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.conj
Plain-language statement
Crucial inducion for formalized -completeness.
Source project: Foundation
Person-level attribution pending.