diff --git a/src/first_order/arithmetics.md b/src/first_order/arithmetics.md
index 118c875..07aab25 100644
--- a/src/first_order/arithmetics.md
+++ b/src/first_order/arithmetics.md
@@ -81,33 +81,33 @@ Since `Exponential` and `Exponential.total` are defined in all the model of $\ma
 |           $\mathrm{Semiformula}_x(y)$           | [`L.Semiformula x y`]   |           $\mathsf{I}\Sigma_1$           |                    -                     | $\Delta_1$ |        -         |
 
 [`x ≤ y`]: https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Arith/PeanoMinus.html#LO.Arith.instLE_logic
-[`x - y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/PeanoMinus.html#LO.Arith.sub
-[`x ∣ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/PeanoMinus.html#LO.FirstOrder.Arith.dvd
-[`x / y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.instDiv_arithmetization
-[`x % y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.rem
-[`√x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.sqrt
-[`⟪x, y⟫`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pair
-[`π₁ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%81
-[`π₂ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%82
-[`exp x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential
-[`log x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.log
-[`‖x‖`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.binaryLength
-[`x # y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/OmegaOne/Basic.html#LO.Arith.instHash
-[`nuon x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/OmegaOne/Nuon.html#LO.Arith.nuon
-[`x ∈ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.Bit
-[`∅`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instEmptyCollection_arithmetization
-[`x ⊆ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instHasSubset_arithmetization
-[`⋃ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sUnion
-[`x ∪ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union
-[`x ∩ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter
-[`⋂ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sInter
-[`x ×ʰᶠ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product
-[`domain x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.domain
-[`IsMapping x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping
-[`Seq x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq
-[`lh x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.lh
-[`x ⁀' y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.seqCons
-[`znth x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.znth
-[`L.Semiterm x y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Term/Basic.html#LO.Arith.Language.Semiterm
-[`L.termSubst n m w t`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Term/Functions.html#LO.Arith.Language.termSubst
-[`L.Semiformula x y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Formula/Basic.html#LO.Arith.Language.Semiformula
+[`x - y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/PeanoMinus.html#LO.Arith.sub
+[`x ∣ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/PeanoMinus.html#LO.FirstOrder.Arith.dvd
+[`x / y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.instDiv_arithmetization
+[`x % y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.rem
+[`√x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.sqrt
+[`⟪x, y⟫`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pair
+[`π₁ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%81
+[`π₂ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%82
+[`exp x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential
+[`log x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.log
+[`‖x‖`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.binaryLength
+[`x # y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/OmegaOne/Basic.html#LO.Arith.instHash
+[`nuon x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/OmegaOne/Nuon.html#LO.Arith.nuon
+[`x ∈ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.Bit
+[`∅`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instEmptyCollection_arithmetization
+[`x ⊆ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instHasSubset_arithmetization
+[`⋃ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sUnion
+[`x ∪ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union
+[`x ∩ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter
+[`⋂ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sInter
+[`x ×ʰᶠ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product
+[`domain x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.domain
+[`IsMapping x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping
+[`Seq x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq
+[`lh x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.lh
+[`x ⁀' y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.seqCons
+[`znth x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.znth
+[`L.Semiterm x y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Term/Basic.html#LO.Arith.Language.Semiterm
+[`L.termSubst n m w t`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Term/Functions.html#LO.Arith.Language.termSubst
+[`L.Semiformula x y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Formula/Basic.html#LO.Arith.Language.Semiformula
diff --git a/src/first_order/isigma0.md b/src/first_order/isigma0.md
index c1103e3..9047642 100644
--- a/src/first_order/isigma0.md
+++ b/src/first_order/isigma0.md
@@ -11,7 +11,7 @@ and its inductive properties are proved in $\mathsf{I}\Sigma_0$.
 instance exponential_definable [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)
 ```
 
-- [LO.FirstOrder.Arith.Model.exponential_definable](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.exponential_definable)
+- [LO.Arith.exponential_definable](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.exponential_definable)
 
 ![Import Graph](./exp.png)
 
@@ -20,13 +20,13 @@ lemma exponential_zero_one [M ⊧ₘ* 𝐈𝚺₀] :
     Exponential 0 1
 ```
 
-- [LO.FirstOrder.Arith.Model.Exponential.exponential_zero_one](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exponential.exponential_zero_one)
+- [LO.Arith.Exponential.exponential_zero_one](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential.exponential_zero_one)
 
 ```lean
 lemma exponential_succ_mul_two [M ⊧ₘ* 𝐈𝚺₀] {x y : M} :
     Exponential (x + 1) (2 * y) ↔ Exponential x y
 ```
 
-- [LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_two](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_two)
+- [LO.Arith.Exponential.exponential_succ_mul_two](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential.exponential_succ_mul_two)
 
 Other basic functions, such as $\log x, |x|$ are defined by using exponential.
diff --git a/src/first_order/isigma1.md b/src/first_order/isigma1.md
index 90fe798..9070769 100644
--- a/src/first_order/isigma1.md
+++ b/src/first_order/isigma1.md
@@ -16,7 +16,7 @@ Weak theory of sets in $V_\omega$ (Hereditary Finite Sets) can be developed insi
 lemma mem_iff_bit [M ⊧ₘ* 𝐈𝚺₁] {i a : M} : i ∈ a ↔ Bit i a
 ```
 
-- [LO.FirstOrder.Arith.Model.mem_iff_bit](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.FirstOrder.Arith.Model.mem_iff_bit)
+- [LO.Arith.mem_iff_bit](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.mem_iff_bit)
 
 The following comprehension holds.
 
@@ -26,11 +26,11 @@ theorem finset_comprehension₁ [M ⊧ₘ* 𝐈𝚺₁]
     ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
 ```
 
-- [LO.FirstOrder.Arith.Model.finset_comprehension₁](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.FirstOrder.Arith.Model.finset_comprehension%E2%82%81)
+- [LO.Arith.finset_comprehension₁](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.finset_comprehension%E2%82%81)
 
-The basic concepts of set theory, such as [union](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.union), [inter](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.inter),
-[cartesian product](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.product),
-and [mapping](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.IsMapping), etc. are defined.
+The basic concepts of set theory, such as [union](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union), [inter](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter),
+[cartesian product](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product),
+and [mapping](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping), etc. are defined.
 
 ### Seq
 
@@ -40,7 +40,7 @@ $\mathrm{Seq}(s)$ iff $s$ is a mapping and its domain is $[0, l)$ for some $l$.
 def Seq [M ⊧ₘ* 𝐈𝚺₁] (s : M) : Prop := IsMapping s ∧ ∃ l, domain s = under l
 ```
 
-- [LO.FirstOrder.Arith.Model.Seq](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.FirstOrder.Arith.Model.Seq)
+- [LO.Arith.Seq](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq)
 
 ### Primitive Recursion
 
@@ -76,7 +76,7 @@ theorem Construction.result_succ (u : M) :
     c.result v (u + 1) = c.succ v u (c.result v u)
 ```
 
-- [Formulae](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Formulae), [Construction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction), [Construction.result](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result), [Construction.result_zero](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result_zero), [Construction.result_succ](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result_succ)
+- [Formulae](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Formulae), [Construction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction), [Construction.result](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result), [Construction.result_zero](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result_zero), [Construction.result_succ](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result_succ)
 
 ### Fixpoint
 
@@ -114,7 +114,7 @@ theorem Construction.case :
     c.Fixpoint v x ↔ c.Φ v {z | c.Fixpoint v z} x
 ```
 
-- [Blueprint](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Blueprint), [Construction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction), [Construction.Finite](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Finite), [Construction.Fixpoint](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction.Fixpoint), [Construction.case](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction.case)
+- [Blueprint](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Blueprint), [Construction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction), [Construction.Finite](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Finite), [Construction.Fixpoint](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Fixpoint), [Construction.case](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.case)
 
 $\mathsf{Fix}_\Phi(\vec v, x)$ is $\Delta_1$ if $\Phi$ satisfies strong finiteness:
 
@@ -123,7 +123,7 @@ class Construction.StrongFinite (c : Construction M φ) where
   strong_finite {C : Set M} {v x} : c.Φ v C x → c.Φ v {y ∈ C | y < x} x
 ```
 
-- [StrongFinite](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.StrongFinite)
+- [StrongFinite](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.StrongFinite)
 
 Also structural induction holds.
 
@@ -134,4 +134,4 @@ theorem Construction.induction [c.StrongFinite]
     ∀ x, c.Fixpoint v x → P x
 ```
 
-- [LO.Arith.Fixpoint.Construction.induction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.induction)
+- [LO.Arith.Fixpoint.Construction.induction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.induction)