Step
*
1
2
of Lemma
lg-edge-append
.....wf.....
1. [T] : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
4. a : ℕlg-size(g1) + lg-size(g2)@i
5. b : ℕlg-size(g1) + lg-size(g2)@i
6. g2 ∈ Top List
7. b < lg-size(g1)
⊢ T × ℕlg-size(g1) List × (ℕlg-size(g1) List) ∈ 𝕌{[1 | i 0]}
BY
{ Auto }
Latex:
Latex:
.....wf.....
1. [T] : Type
2. g1 : LabeledGraph(T)@i
3. g2 : LabeledGraph(T)@i
4. a : \mBbbN{}lg-size(g1) + lg-size(g2)@i
5. b : \mBbbN{}lg-size(g1) + lg-size(g2)@i
6. g2 \mmember{} Top List
7. b < lg-size(g1)
\mvdash{} T \mtimes{} \mBbbN{}lg-size(g1) List \mtimes{} (\mBbbN{}lg-size(g1) List) \mmember{} \mBbbU{}\{[1 | i 0]\}
By
Latex:
Auto
Home
Index