---

Step * 1 1 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
⊢ f ∈ x:LabeledGraph(T) ─→ {y:LabeledGraph(T)| x = y ∈ LabeledGraph(T)} 
BY
{ (ExtWith [`G'] [⌈x:((T × ℤ List × (ℤ List)) List) ─→ {y:(T × ℤ List × (ℤ List)) List| 
                                                        x = y ∈ ((T × ℤ List × (ℤ List)) List)} ⌉]⋅
   THEN Auto
   )⋅ }

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)
⊢ f G ∈ {y:LabeledGraph(T)| G = y ∈ LabeledGraph(T)} 

---

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
\mvdash{}  f  \mmember{}  x:LabeledGraph(T)  {}\mrightarrow{}  \{y:LabeledGraph(T)|  x  =  y\} 


By

---

Latex:
(ExtWith  [`G']  [\mkleeneopen{}x:((T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List)  {}\mrightarrow{}  \{y:(T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List|  x  =  y\}  \mkleeneclose{}]\mcdot{}
  THEN  Auto
  )\mcdot{}

---

Home Index