---

Step * 2 of Lemma lg-remove_wf


1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ (T × ℕ||lg-remove(g;x)|| List × (ℕ||lg-remove(g;x)|| List)) List
BY
{ Subst' ⌈||lg-remove(g;x)|| = if x <z ||g|| then ||g|| - 1 else ||g|| fi  ∈ ℤ⌉ 0⋅ }

1
.....equality..... 
1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ ||lg-remove(g;x)|| = if x <z ||g|| then ||g|| - 1 else ||g|| fi  ∈ ℤ

2
1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ (T
  × ℕif x <z ||g|| then ||g|| - 1 else ||g|| fi  List
  × (ℕif x <z ||g|| then ||g|| - 1 else ||g|| fi  List)) List

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  self:Top  List  \mcap{}  (T  \mtimes{}  \mBbbN{}||self||  List  \mtimes{}  (\mBbbN{}||self||  List))  List
3.  g  \mmember{}  Top  List
4.  g  \mmember{}  (T  \mtimes{}  \mBbbN{}||g||  List  \mtimes{}  (\mBbbN{}||g||  List))  List
5.  ||g||  \mmember{}  \mBbbN{}
6.  x  :  \mBbbN{}
\mvdash{}  lg-remove(g;x)  \mmember{}  (T  \mtimes{}  \mBbbN{}||lg-remove(g;x)||  List  \mtimes{}  (\mBbbN{}||lg-remove(g;x)||  List))  List


By

---

Latex:
Subst'  \mkleeneopen{}||lg-remove(g;x)||  =  if  x  <z  ||g||  then  ||g||  -  1  else  ||g||  fi  \mkleeneclose{}  0\mcdot{}

---

Home Index