Step
*
1
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
3. G : LabeledGraph(T)
⊢ f G ∈ {y:LabeledGraph(T)| G = y ∈ LabeledGraph(T)}
BY
{ (GenConclAtAddr [2] 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)
⊢ G ∈ (T × ℤ List × (ℤ List)) List
2
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. y : (T × ℤ List × (ℤ List)) List@i
⊢ G ∈ (T × ℤ List × (ℤ List)) List
3
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 : {y:(T × ℤ List × (ℤ List)) List| G = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
5. (f G) = v ∈ {y:(T × ℤ List × (ℤ List)) List| G = y ∈ ((T × ℤ List × (ℤ List)) List)} @i
⊢ v ∈ {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
3. G : LabeledGraph(T)
\mvdash{} f G \mmember{} \{y:LabeledGraph(T)| G = y\}
By
Latex:
(GenConclAtAddr [2] THEN Auto)
Home
Index