RewThree

Abstract

Licensed Foundation.Syntax.Predicate.Rew source selected from the historical first-order pair extension.

This document mirrors the retained declarations from Foundation.Syntax.Predicate.Rew, lines 638-953, at Foundation revision 30a16ffa93d79d73ab4d02427fa00f50e039bf29. The excerpt records the term-rewriting laws and interfaces associated with the concrete first-order pair extension; current downstream consumer usage has not been re-queried.

The immutable source map, modification notices, full Apache-2.0 license and retirement condition are in Library/ConceptDynamics/foundation2026firstorder.md.

Lemma 1.1 (Fixing bound variables preserves the variable with an enlarged finite index).

$$\forall n,m:\mathbb{N},\forall x:\mathrm{Fin}\left(n\right),\mathrm{fixitr}\left(n,m,\mathrm{bvar}\left(x\right)\right)=\mathrm{bvar}\left(\mathrm{castAdd}\left(x,m\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.fixitr_bvar (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

For every finite bound index x, fixing m variables maps the bound variable to its castAdd representative in the enlarged context.

Lemma 1.2 (Fixing free variables either binds or shifts them).

$$\forall n,m,x\in \mathbb{N},\mathrm{fixitr}\left(n,m,\mathrm{fvar}\left(x\right)\right)=\mathrm{if}\left(\mathrm{lt}\left(x,m\right),\mathrm{bvar}\left(\mathrm{natAdd}\left(n,\mathrm{pair}\left(x,\mathrm{proof}\left(x,m\right)\right)\right)\right),\mathrm{fvar}\left(x-m\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.fixitr_fvar (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

A free variable below the fixed prefix becomes a bound variable; otherwise its index is decreased by the prefix length.

Lemma 1.3 (Rewrites agree when they agree on the variables visible in a term).

$$\forall omega1,omega2,t(\mathrm{agreeBvar}\left(omega1,omega2\right)\wedge \mathrm{agreeOn}\left(\mathrm{fvarSupport}\left(t\right),omega1,omega2\right))\Rightarrow \mathrm{eq}\left(\mathrm{apply}\left(omega1,t\right),\mathrm{apply}\left(omega2,t\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.rew_eq_of_funEqOn (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Agreement on every bound variable and on the free variables occurring in the term is sufficient for equality after rewriting that term.

Lemma 1.4 (Language maps commute with term binding).

$$\forall phi,b,e,t\mathrm{lMap}\left(phi,\mathrm{bind}\left(b,e,t\right)\right)=\mathrm{bind}\left(\mathrm{compose}\left(\mathrm{lMap}\left(phi\right),b\right),\mathrm{compose}\left(\mathrm{lMap}\left(phi\right),e\right),\mathrm{lMap}\left(phi,t\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_bind (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Mapping function symbols through a language homomorphism commutes with binding both bound and free variables.

Lemma 1.5 (Language maps commute with variable maps).

$$\forall phi,b,e,t\mathrm{lMap}\left(phi,\mathrm{map}\left(b,e,t\right)\right)=\mathrm{map}\left(b,e,\mathrm{lMap}\left(phi,t\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_map (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The map that changes variable indices and free-variable labels commutes with the language map on terms.

Lemma 1.6 (Language maps commute with bound-variable shifting).

$$\forall phi,t\mathrm{lMap}\left(phi,\mathrm{bShift}\left(t\right)\right)=\mathrm{bShift}\left(\mathrm{lMap}\left(phi,t\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_bShift (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Adding one bound-variable slot before or after a language map gives the same term.

Lemma 1.7 (A free variable after rewriting comes from a source variable (the canonical selector is RewThreeCompat.fvar_rew; the source name is fvar?_rew).).

$$\forall omega,t,x\mathrm{fvarAt}\left(\mathrm{apply}\left(omega,t\right),x\right)\Rightarrow ((\exists i:\mathrm{Fin}\left(n1\right),\mathrm{fvarAt}\left(\mathrm{apply}\left(omega,\mathrm{bvar}\left(i\right)\right),x\right))\vee (\exists z:xi1,(\mathrm{contains}\left(\mathrm{fvarSupport}\left(t\right),z\right)\wedge \mathrm{fvarAt}\left(\mathrm{apply}\left(omega,\mathrm{fvar}\left(z\right)\right),x\right)))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.fvar_rew (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

If a free variable occurs in a rewritten term, it came either from a rewritten bound variable or from a free variable of the source term.

Lemma 1.8 (Bound-variable shifting preserves free-variable support (the canonical selector is RewThreeCompat.fvar_bShift; the source name is fvar?_bShift).).

$$\forall t,x\mathrm{fvarAt}\left(\mathrm{bShift}\left(t\right),x\right)\iff \mathrm{fvarAt}\left(t,x\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.fvar_bShift (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The bShift operation changes only bound indices, so the set of free variables is unchanged.

Definition 1.9 (A term with no free variables is converted to an empty-variable term).

$$\begin{array}{r}toEmpty:\forall n:\mathbb{N},\forall t:\mathrm{Semiterm}\left(L,xi,n\right),h:\mathrm{freeVariables}\left(t\right)=\varnothing \Rightarrow \mathrm{ClosedSemiterm}\left(L,n\right)\\ \mathrm{toEmpty}\left(\mathrm{bvar}\left(x\right),h\right)=\mathrm{bvar}\left(x\right)\text{where}x:\mathrm{Fin}\left(n\right),h:\mathrm{freeVariables}\left(\mathrm{bvar}\left(x\right)\right)=\varnothing \\ \mathrm{toEmpty}\left(\mathrm{fvar}\left(z\right),h\right)=\mathrm{impossible}\left(h\right)\text{where}h:\mathrm{freeVariables}\left(\mathrm{fvar}\left(z\right)\right)=\varnothing \\ \mathrm{toEmpty}\left(\mathrm{func}\left(f,v\right),h\right)=\mathrm{func}\left(f,i\mapsto \mathrm{toEmpty}\left(\mathrm{at}\left(v,i\right),hi\right)\right)\text{where}\forall i:\mathrm{Fin}\left(k\right),hi:\mathrm{freeVariables}\left(\mathrm{at}\left(v,i\right)\right)=\varnothing \end{array}$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.toEmpty (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The dependent definition recurses by cases: a bound variable is returned unchanged, a free-variable case is impossible from its empty-support proof, and a function node is rebuilt from recursively converted arguments, each carrying the empty-support proof derived from the parent.

Lemma 1.10 (Embedding the empty-variable form recovers the original term).

$$\forall t\mathrm{freeVariables}\left(t\right)=\varnothing \Rightarrow \mathrm{emb}\left(\mathrm{toEmpty}\left(t\right)\right)=t.$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.emb_toEmpty (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The retained structural induction proves that embedding the term produced by toEmpty recovers the original term.

Definition 1.11 (A rewriting action applies rewrites to formulas and respects quantifiers).

$$\mathrm{Rewriting}\left(L,xi,F,zeta,G\right)=(app:\forall n1:\mathbb{N},n2:\mathbb{N},\mathrm{Rew}\left(L,xi,n1,zeta,n2\right)\to \mathrm{Hom}\left(F\left(n1\right),G\left(n2\right)\right),\forall n1:\mathbb{N},n2:\mathbb{N},omega12:\mathrm{Rew}\left(L,xi,n1,zeta,n2\right),phi:F\left(n1+1\right),\mathrm{appAll}\left(omega12,phi\right):\mathrm{app}\left(omega12,forall1\left(phi\right)\right)=forall1\left(\mathrm{app}\left(q\left(omega12\right),phi\right)\right)\wedge \mathrm{appExs}\left(omega12,phi\right):\mathrm{app}\left(omega12,exists1\left(phi\right)\right)=exists1\left(\mathrm{app}\left(q\left(omega12\right),phi\right)\right)).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.Rewriting (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

A Rewriting instance supplies an action of term rewrites on formulas, with universal and existential quantification transported through the rewrite. The app field is indexed by both bound-variable sizes; app_all and app_exs each take φ:F(n1+1) and use the lifted rewrite q(ω):Rew(L,ξ,n1+1,ζ,n2+1).

Definition 1.12 (Formula substitution is the substitution rewrite action).

$$\forall n1:\mathbb{N},n2:\mathbb{N},phi:F\left(n1\right),w:\mathrm{Fin}\left(n1\right)\to \mathrm{Semiterm}\left(L,xi,n2\right),\mathrm{subst}\left(phi,w\right)=\mathrm{app}\left(\mathrm{RewSubst}\left(w\right),phi\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.subst (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

For every indexed formula φ and substitution vector w:Fin(n1)→Semiterm(L,ξ,n2), the abbreviation subst(φ,w) is exactly app(Rew.subst(w),φ) through the Rewriting action.

Definition 1.13 (Formula shift is the shift rewrite action).

$$shift:\mathrm{Hom}\left(F\left(n\right),F\left(n\right)\right)=\mathrm{app}\left(RewShift\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.shift (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The shift connective homomorphism applies Rew.shift to formulas while increasing free-variable indices.

Definition 1.14 (Formula free operation removes the last bound-variable slot).

$$free:\mathrm{Hom}\left(F\left(n+1\right),F\left(n\right)\right)=\mathrm{app}\left(RewFree\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.free (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The free connective homomorphism maps the last bound slot to free variable &0 and shifts each existing free variable &m to &(m+1), taking formulas from the n+1 bound-variable context to the n context.

Definition 1.15 (Formula-list shift maps each member).

$$shifts:\mathrm{List}\left(F\left(n\right)\right)\to \mathrm{List}\left(F\left(n\right)\right)=\mathrm{map}\left(shift\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.shifts (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The shifts definition maps the shift homomorphism over a finite list of formulas.

Lemma 1.16 (Shifting an empty formula list stays empty).

$$\mathrm{shifts}\left([]\right)=[].$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_nil (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The ASCII compatibility selector forwards the source shifts_nil theorem, including its exact LCWQ and Rewriting assumptions.

Lemma 1.17 (Shifting a cons list shifts its head and tail).

$$\mathrm{shifts}\left(\mathrm{cons}\left(phi,Gamma\right)\right)=\mathrm{cons}\left(\mathrm{shift}\left(phi\right),\mathrm{shifts}\left(Gamma\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_cons (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The ASCII compatibility selector forwards the source shifts_cons theorem pointwise over the head and tail.

Lemma 1.18 (Shifting a negated formula list commutes with negation).

$$\mathrm{shifts}\left(\mathrm{negList}\left(Gamma\right)\right)=\mathrm{negList}\left(\mathrm{shifts}\left(Gamma\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_neg (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The ASCII compatibility selector forwards the source shifts_neg theorem for list negation.

Definition 1.19 (Empty-label formulas embed as connective homomorphisms).

$$emb:\mathrm{Hom}\left(O\left(n\right),F\left(n\right)\right)=\mathrm{app}\left(RewEmb\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.emb (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

The ASCII compatibility selector exposes the source emb connective homomorphism from an empty-label family O to a ξ-labelled family F.

Definition 1.20 (Typed substitution selector agrees with slash-vector syntax).

$$\forall phi:S\left(1\right),\mathrm{substNotation}\left(phi,\mathrm{Matrix}.\mathrm{vecCons}(\mathrm{fvar}\left(0\right),\mathrm{Matrix}.\mathrm{vecEmpty})\right)=phi/[\mathrm{fvar}\left(0\right)]=\mathrm{subst}\left(phi,\mathrm{Matrix}.\mathrm{vecCons}(\mathrm{fvar}\left(0\right),\mathrm{Matrix}.\mathrm{vecEmpty})\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.substNotation (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Under [LCWQ S] and [SyntacticRewriting L S S], the typed compatibility selector substNotation(φ,w) forwards Rewriting.subst(φ,w). The source slash syntax φ/[t] expands to φ ⇜ ![t]. For the one-entry vector used below, ![&0] is Matrix.vecCons(fvar(0), Matrix.vecEmpty).

Definition 1.21 (The identity rewrite acts as the identity on formulas).

$$\forall phi\mathrm{app}\left(\mathrm{id}\left(L\right),phi\right)=phi.$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.ReflectiveRewriting (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Reflectivity records that applying Rew.id leaves every formula unchanged.

Definition 1.22 (Composed rewrites act by successive formula application).

$$\forall omega12,omega23,phi\mathrm{app}\left(\mathrm{comp}\left(omega23,omega12\right),phi\right)=\mathrm{app}\left(omega23,\mathrm{app}\left(omega12,phi\right)\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.TransitiveRewriting (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Transitivity identifies application of a composed rewrite with applying the first rewrite and then the second.

Definition 1.23 (Injective variable and label maps induce an injective formula action).

$$\forall b,f(\mathrm{Injective}\left(b\right)\wedge \mathrm{Injective}\left(f\right))\Rightarrow \mathrm{Injective}\left(\mathrm{mapAction}\left(b,f\right)\right).$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.InjMapRewriting (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

If both the bound-variable map and free-variable map are injective, the induced map on formulas is injective.

Definition 1.24 (Lawful syntactic rewriting combines identity, composition and injectivity).

$$\begin{array}{r}\mathrm{LawfulSyntacticRewriting}\left(L,S\right)(L:Language,S:\mathbb{N}\to Type)[\mathrm{LCWQ}\left(S\right)][\mathrm{SyntacticRewriting}\left(L,S,S\right)]\\ \text{extends}(\mathrm{ReflectiveRewriting}\left(L,\mathbb{N},S\right),\mathrm{TransitiveRewriting}\left(L,\mathbb{N},S,\mathbb{N},S,\mathbb{N},S\right),\mathrm{InjMapRewriting}\left(L,\mathbb{N},S,\mathbb{N},S\right)).\end{array}$$

Formalization. D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.LawfulSyntacticRewriting (✓ std3).

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

With [LCWQ S] and [SyntacticRewriting L S S] as its parameters, the class extends ReflectiveRewriting L ℕ S, TransitiveRewriting L ℕ S ℕ S ℕ S, and InjMapRewriting L ℕ S ℕ S. These are inherited interfaces, not a proposition asserted by an equality.

Lemma 1.25 (Shifting a conjunction shifts each formula (the canonical selector is RewThreeCompat.shift_conj_two; the source name is shift_conj₂).).

$$[\mathrm{LCWQ}\left(S\right)][\mathrm{SyntacticRewriting}\left(L,S,S\right)]\Rightarrow \forall n:\mathbb{N},\forall Gamma:\mathrm{List}\left(S\left(n\right)\right),\mathrm{shift}\left(\mathrm{conj}\left(Gamma\right)\right)=\mathrm{conj}\left(\mathrm{map}\left(shift,Gamma\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shift_conj_two (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

Under [LCWQ S] and [SyntacticRewriting L S S], for Γ:List(S n), the shift of a finite conjunction is the conjunction of the list mapped by shift:S n→S n, including the empty and singleton cases.

Lemma 1.26 (Substituting the first free variable after shifting is free).

$$[\mathrm{LCWQ}\left(S\right)][\mathrm{SyntacticRewriting}\left(L,S,S\right)][\mathrm{LawfulSyntacticRewriting}\left(L,S\right)]\Rightarrow \forall phi:S\left(1\right),\mathrm{subst}\left(\mathrm{shift}\left(phi\right),\mathrm{Matrix}.\mathrm{vecCons}(\mathrm{fvar}\left(0\right),\mathrm{Matrix}.\mathrm{vecEmpty})\right)=\mathrm{free}\left(phi\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.app_subst_fbar_zero_comp_shift_eq_free (✓ std3). ∎

Citation. FormalizedFormalLogic contributors (2026). Foundation first-order logic and set theory, revision 30a16ffa. URL: https://github.com/FormalizedFormalLogic/Foundation/tree/30a16ffa93d79d73ab4d02427fa00f50e039bf29.

Commentary.

For a one-variable formula, shifting and substituting the zero free variable agrees with the free operation. The substitution vector is the explicit one-entry Matrix.vecCons(fvar(0), Matrix.vecEmpty), and the law is stated under the LCWQ, SyntacticRewriting, and LawfulSyntacticRewriting context.

References

• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.InjMapRewriting
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.LawfulSyntacticRewriting
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.ReflectiveRewriting
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.Rewriting
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.TransitiveRewriting
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.emb_toEmpty
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.fixitr_bvar
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.fixitr_fvar
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.free
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_bShift
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_bind
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.lMap_map
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.rew_eq_of_funEqOn
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.shift
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.shifts
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.subst
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThree.toEmpty
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.app_subst_fbar_zero_comp_shift_eq_free
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.emb
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.fvar_bShift
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.fvar_rew
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shift_conj_two
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_cons
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_neg
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.shifts_nil
• Truth anchor: D5/S3/ConceptDynamics/ZfcTermRewriting/RewThreeCompat.substNotation
• Dependency: D5/S3/ConceptDynamics/ZfcPredicate/Quantifier
• Dependency: D5/S3/ConceptDynamics/ZfcPredicate/Term
• Dependency: D5/S3/ConceptDynamics/ZfcSupport/Function
• Dependency: D5/S3/ConceptDynamics/ZfcTermRewriting/RewTwo