Le term BShift
LO.FirstOrder.Arithmetic.Bootstrapping.le_termBShift
Plain-language statement
termBShift only grows codes: t ≤ termBShift t for well-formed terms. The ^#z → ^#(z+1) bvar shift grows, ^&x is fixed, and functions recurse componentwise. Bounds the ∃ t guard in the bounded-∀ clause.
Exact Lean statement
lemma le_termBShift {t : V} (ht : IsUTerm L t) : t ≤ termBShift L tFormal artifact
Lean source
lemma le_termBShift {t : V} (ht : IsUTerm L t) : t ≤ termBShift L t := by refine IsUTerm.induction 𝚺 (P := fun t ↦ t ≤ termBShift L t) ?_ ?_ ?_ ?_ t ht · definability · intro z rw [termBShift_bvar] simp only [qqBvar] exact add_le_add (pair_le_pair_right (0 : V) le_self_add) (le_refl 1) · intro x; simp · intro k f v hf hv ih rw [termBShift_func hf hv] have hvle : v ≤ termBShiftVec L k v := by refine le_of_nth_le_nth ?_ ?_ · rw [len_termBShiftVec hv]; exact hv.1.symm · intro i hi rw [← hv.1] at hi rw [nth_termBShiftVec hv hi] exact ih i hi simp only [qqFunc] exact add_le_add (pair_le_pair_right 2 (pair_le_pair_right k (pair_le_pair_right f hvle))) (le_refl 1)- Project
- Foundation
- License
- Apache-2.0
- Commit
- 8dcdb3196454
- Source
- Foundation/FirstOrder/Incompleteness/InductionSchemeDelta1.lean:488-507
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.