LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Bootstrapping.Syntax.Term.Coding

Supporting results for pointwise provable equality.

noncomputable def PointwiseComposition.FFL.FirstOrder.Semiterm.typedQuote (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

SyntacticSemiterm L n → Arithmetic.Bootstrapping.Semiterm V L n

The typed Quote construction in FFL.FirstOrder.Semiterm.

Equations

One or more equations did not get rendered due to their size.
PointwiseComposition.FFL.FirstOrder.Semiterm.typedQuote V (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar x_1) = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Semiterm.bvar x_1
PointwiseComposition.FFL.FirstOrder.Semiterm.typedQuote V (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar x_1) = PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Semiterm.fvar ↑x_1

Instances For

source

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemitermSemiterm (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (SyntacticSemiterm L n) (Arithmetic.Bootstrapping.Semiterm V L n)

Equations

PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemitermSemiterm V = { quote := PointwiseComposition.FFL.FirstOrder.Semiterm.typedQuote V }

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :

⌜bvar x⌝ = Arithmetic.Bootstrapping.Semiterm.bvar x

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_fvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : ℕ) :

⌜fvar x⌝ = Arithmetic.Bootstrapping.Semiterm.fvar ↑x

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) :

⌜func f v⌝ = Arithmetic.Bootstrapping.Semiterm.func f fun (i : Fin k) => ⌜v i⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

⌜Rew.shift t⌝ = ⌜t⌝.shift

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_bShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

⌜Rew.bShift t⌝ = ⌜t⌝.bShift

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m : ℕ} (t : SyntacticSemiterm L n) (w : Fin n → SyntacticSemiterm L m) :

⌜(Rew.subst w) t⌝ = Arithmetic.Bootstrapping.Semiterm.subst (fun (i : Fin n) => ⌜w i⌝) ⌜t⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜‘(!!t + !!u)’⌝ = ⌜t⌝ + ⌜u⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (t u : SyntacticSemiterm ℒₒᵣ n) :

⌜‘(!!t * !!u)’⌝ = ⌜t⌝ * ⌜u⌝

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_numeral_eq_numeral_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} :

⌜↑1⌝ = Arithmetic.Bootstrapping.ObjectArithmetic.typedNumeral 1

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_numeral_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (k : ℕ) :

⌜↑k⌝ = Arithmetic.Bootstrapping.ObjectArithmetic.typedNumeral ↑k

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {t u : SyntacticSemiterm L n} :

⌜t⌝ = ⌜u⌝ → t = u

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.typed_quote_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} {t u : SyntacticSemiterm L n} :

⌜t⌝ = ⌜u⌝ ↔ t = u

source

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (SyntacticSemiterm L n) V

Equations

PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteSyntacticSemiterm = { quote := fun (t : PointwiseComposition.FFL.FirstOrder.SyntacticSemiterm L n) => ⌜t⌝.val }

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

⌜t⌝ = ⌜t⌝.val

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

⌜t⌝ = ↑(Encodable.encode t)

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_eq_encode' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (v : Fin k → Semiterm L ℕ n) :

(Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝) = ↑(Matrix.vecToNat fun (i : Fin k) => Encodable.encode (v i))

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_eq_encode_standard {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

⌜t⌝ = Encodable.encode t

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.coe_quote_eq_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

↑⌜t⌝ = ⌜t⌝

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.coe_quote_eq_quote' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : SyntacticSemiterm L n) :

↑⌜t⌝.val = ⌜t⌝.val

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :

⌜bvar x⌝ = Arithmetic.Bootstrapping.qqBvar ↑↑x

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_fvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : ℕ) :

⌜fvar x⌝ = Arithmetic.Bootstrapping.qqFvar ↑x

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → SyntacticSemiterm L n) :

⌜func f v⌝ = Arithmetic.Bootstrapping.qqFunc ↑k ⌜f⌝ (Arithmetic.Bootstrapping.SemitermVec.val fun (i : Fin k) => ⌜v i⌝)

source

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteClosedSemitermSemiterm (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (ClosedSemiterm L n) (Arithmetic.Bootstrapping.Semiterm V L n)

Equations

One or more equations did not get rendered due to their size.

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :

⌜t⌝ = ⌜Rew.emb t⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_bvar {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (x : Fin n) :

⌜bvar x⌝ = Arithmetic.Bootstrapping.Semiterm.bvar x

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_func {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k : ℕ} (f : L.Func k) (v : Fin k → ClosedSemiterm L n) :

⌜func f v⌝ = Arithmetic.Bootstrapping.Semiterm.func f fun (i : Fin k) => ⌜v i⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜‘(!!t + !!u)’⌝ = ⌜t⌝ + ⌜u⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (t u : ClosedSemiterm ℒₒᵣ n) :

⌜‘(!!t * !!u)’⌝ = ⌜t⌝ * ⌜u⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_typed_quote_numeral_eq_numeral {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {n : ℕ} (k : ℕ) :

⌜↑k⌝ = Arithmetic.Bootstrapping.ObjectArithmetic.typedNumeral ↑k

source

@[instance_reducible]

noncomputable instance PointwiseComposition.FFL.FirstOrder.Semiterm.instGödelQuoteClosedSemiterm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} :

GödelQuote (ClosedSemiterm L n) V

Equations

One or more equations did not get rendered due to their size.

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_quote_def {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :

⌜t⌝ = ⌜Rew.emb t⌝

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_quote_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :

⌜t⌝ = ⌜t⌝.val

source

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.empty_quote_eq_encode {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : ℕ} (t : ClosedSemiterm L n) :

⌜t⌝ = ↑(Encodable.encode t)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.coe_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (t : SyntacticSemiterm L n) :

↑⌜t⌝ = ⌜t⌝

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.coe_empty_quote {L : Language} [L.Encodable] [L.LORDefinable] {m : ℕ} {ξ : Type u_2} {n : ℕ} (t : ClosedSemiterm L n) :

↑⌜t⌝ = ⌜t⌝

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.mem_iff_mem_bitIndices {x s : ℕ} :

x ∈ s ↔ x ∈ s.bitIndices

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.nat_mem_iff {x s : ℕ} :

x ∈ s ↔ s / 2 ^ x % 2 = 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.nat_insert_eq (x s : ℕ) :

insert x s = if s / 2 ^ x % 2 = 1 then s else s + 2 ^ x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiterm.sound {L : Language} [L.Encodable] [L.LORDefinable] {n t : ℕ} (ht : IsSemiterm L n t) :

∃ (T : SyntacticSemiterm L n), ⌜T⌝ = t