---

Step * of Lemma lg-edge-append

∀[T:Type]
  ∀g1,g2:LabeledGraph(T). ∀a,b:ℕlg-size(g1) + lg-size(g2).
    (lg-edge(lg-append(g1;g2);a;b)
    ⇐⇒ (a < lg-size(g1) ∧ b < lg-size(g1) ∧ lg-edge(g1;a;b))
        ∨ ((lg-size(g1) ≤ a) ∧ (lg-size(g1) ≤ b) ∧ lg-edge(g2;a - lg-size(g1);b - lg-size(g1))))
BY
{ (((UnivCD THENA Auto) THEN (Assert g2 ∈ Top List BY Auto))
   THEN RepUR ``lg-edge lg-in-edges lg-append`` 0
   THEN ((RWW "select-append" 0 THENM Fold `lg-size` 0) THENA Auto)
   THEN (BoolCase ⌜b <z lg-size(g1)⌝⋅ THENA Auto)
   THEN ((RWW "select-map" 0⋅ THENM Reduce 0) THENA Auto)) }

1
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)
⊢ (a ∈ fst(snd(g1[b])))
⇐⇒ (a < lg-size(g1) ∧ b < lg-size(g1) ∧ (a ∈ fst(snd(g1[b]))))
    ∨ ((lg-size(g1) ≤ a) ∧ (lg-size(g1) ≤ b) ∧ (a - lg-size(g1) ∈ fst(snd(g2[b - lg-size(g1)]))))

2
.....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. ¬b < lg-size(g1)
7. g2 ∈ Top List
⊢ b - lg-size(g1) ∈ ℕ||g2||

3
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. ¬b < lg-size(g1)
7. g2 ∈ Top List
⊢ (a ∈ fst(snd(let lbl,in,out = g2[b - lg-size(g1)] in 
   <lbl, map(λx.(x + lg-size(g1));in), map(λx.(x + lg-size(g1));out)>)))
⇐⇒ (a < lg-size(g1) ∧ b < lg-size(g1) ∧ (a ∈ fst(snd(g1[b]))))
    ∨ ((lg-size(g1) ≤ a) ∧ (lg-size(g1) ≤ b) ∧ (a - lg-size(g1) ∈ fst(snd(g2[b - lg-size(g1)]))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}g1,g2:LabeledGraph(T).  \mforall{}a,b:\mBbbN{}lg-size(g1)  +  lg-size(g2).
        (lg-edge(lg-append(g1;g2);a;b)
        \mLeftarrow{}{}\mRightarrow{}  (a  <  lg-size(g1)  \mwedge{}  b  <  lg-size(g1)  \mwedge{}  lg-edge(g1;a;b))
                \mvee{}  ((lg-size(g1)  \mleq{}  a)  \mwedge{}  (lg-size(g1)  \mleq{}  b)  \mwedge{}  lg-edge(g2;a  -  lg-size(g1);b  -  lg-size(g1))))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (Assert  g2  \mmember{}  Top  List  BY  Auto))
  THEN  RepUR  ``lg-edge  lg-in-edges  lg-append``  0
  THEN  ((RWW  "select-append"  0  THENM  Fold  `lg-size`  0)  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}b  <z  lg-size(g1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((RWW  "select-map"  0\mcdot{}  THENM  Reduce  0)  THENA  Auto))

---

Home Index