---

Step * 1 1 1 1 3 2 1 of Lemma norm-lg_wf


1. T : Type
2. f : x:((T × ℤ List × (ℤ List)) List) ─→ {y:(T × ℤ List × (ℤ List)) List| x = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
3. G : LabeledGraph(T)
4. v : (T × ℤ List × (ℤ List)) List@i
5. G = v ∈ ((T × ℤ List × (ℤ List)) List)@i
6. (f G) = v ∈ {y:(T × ℤ List × (ℤ List)) List| G = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
⊢ G = v ∈ ((T × ℕ||G|| List × (ℕ||G|| List)) List)
BY
{ (Assert G ∈ (T × ℕ||G|| List × (ℕ||G|| List)) List BY
         (DVar `G' THEN Hypothesis)) }

1
1. T : Type
2. f : x:((T × ℤ List × (ℤ List)) List) ─→ {y:(T × ℤ List × (ℤ List)) List| x = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
3. G : LabeledGraph(T)
4. v : (T × ℤ List × (ℤ List)) List@i
5. G = v ∈ ((T × ℤ List × (ℤ List)) List)@i
6. (f G) = v ∈ {y:(T × ℤ List × (ℤ List)) List| G = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
7. G ∈ (T × ℕ||G|| List × (ℕ||G|| List)) List
⊢ G = v ∈ ((T × ℕ||G|| List × (ℕ||G|| List)) List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  x:((T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List)  {}\mrightarrow{}  \{y:(T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List|  x  =  y\}  @i
3.  G  :  LabeledGraph(T)
4.  v  :  (T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List@i
5.  G  =  v@i
6.  (f  G)  =  v@i
\mvdash{}  G  =  v


By

---

Latex:
(Assert  G  \mmember{}  (T  \mtimes{}  \mBbbN{}||G||  List  \mtimes{}  (\mBbbN{}||G||  List))  List  BY
              (DVar  `G'  THEN  Hypothesis))

---

Home Index