---

Step * 1 1 1 1 2 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. y : (T × ℤ List × (ℤ List)) List@i
⊢ G ∈ (T × ℤ List × (ℤ List)) List
BY
{ (Assert ⌈G ∈ LabeledGraph(T)⌉⋅
   THEN Auto
   THEN (DVar `G'
         THEN All (Fold `lg-size`)
         THEN SubsumeC ⌈(T × ℕlg-size(G) List × (ℕlg-size(G) List)) List⌉⋅
         THEN Auto
         THEN SubtypeReasoning
         THEN Auto)⋅) }

---

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.  y  :  (T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List@i
\mvdash{}  G  \mmember{}  (T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List


By

---

Latex:
(Assert  \mkleeneopen{}G  \mmember{}  LabeledGraph(T)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (DVar  `G'
              THEN  All  (Fold  `lg-size`)
              THEN  SubsumeC  \mkleeneopen{}(T  \mtimes{}  \mBbbN{}lg-size(G)  List  \mtimes{}  (\mBbbN{}lg-size(G)  List))  List\mkleeneclose{}\mcdot{}
              THEN  Auto
              THEN  SubtypeReasoning
              THEN  Auto)\mcdot{})

---

Home Index