---

Step * 2 2 3 1 1 of Lemma lg-edge-remove


1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
6. Z1 : T@i
7. Z3 : ℕlg-size(g) List@i
8. Z4 : ℕlg-size(g) List@i
9. g[if b <z i then b else b + 1 fi ] = <Z1, Z3, Z4> ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))@i
⊢ ∃y:ℤ. ((y ∈ filter(λx.(¬b(x =z i));Z3)) ∧ (a = if y ≤z i then y else y - 1 fi  ∈ ℤ))
⇐⇒ (if a <z i then a else a + 1 fi  ∈ Z3)
BY
{ ((RWO "member_filter" 0 THEN Reduce 0) THEN Auto) }

1
1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
6. Z1 : T@i
7. Z3 : ℕlg-size(g) List@i
8. Z4 : ℕlg-size(g) List@i
9. g[if b <z i then b else b + 1 fi ] = <Z1, Z3, Z4> ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))@i
10. ∃y:ℤ. (((y ∈ Z3) ∧ (↑¬b(y =z i))) ∧ (a = if y ≤z i then y else y - 1 fi  ∈ ℤ))@i
⊢ (if a <z i then a else a + 1 fi  ∈ Z3)

2
1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
6. Z1 : T@i
7. Z3 : ℕlg-size(g) List@i
8. Z4 : ℕlg-size(g) List@i
9. g[if b <z i then b else b + 1 fi ] = <Z1, Z3, Z4> ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))@i
10. (if a <z i then a else a + 1 fi  ∈ Z3)@i
⊢ ∃y:ℤ. (((y ∈ Z3) ∧ (↑¬b(y =z i))) ∧ (a = if y ≤z i then y else y - 1 fi  ∈ ℤ))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  i  :  \mBbbN{}lg-size(g)@i
4.  a  :  \mBbbN{}lg-size(g)  -  1@i
5.  b  :  \mBbbN{}lg-size(g)  -  1@i
6.  Z1  :  T@i
7.  Z3  :  \mBbbN{}lg-size(g)  List@i
8.  Z4  :  \mBbbN{}lg-size(g)  List@i
9.  g[if  b  <z  i  then  b  else  b  +  1  fi  ]  =  <Z1,  Z3,  Z4>@i
\mvdash{}  \mexists{}y:\mBbbZ{}.  ((y  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  i));Z3))  \mwedge{}  (a  =  if  y  \mleq{}z  i  then  y  else  y  -  1  fi  ))
\mLeftarrow{}{}\mRightarrow{}  (if  a  <z  i  then  a  else  a  +  1  fi    \mmember{}  Z3)


By

---

Latex:
((RWO  "member\_filter"  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index