---

Step * 3 2 1 1 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. a : A@i
⊢ ∀b:B. ((b ∈ reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];L)) ⇐⇒ (<a, b> ∈ L))
BY
{ ((ListInd (-2)) THEN Reduce 0) }

1
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. a : A@i
⊢ ∀b:B. ((b ∈ []) ⇐⇒ (<a, b> ∈ []))

2
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. a : A@i
6. u : A × B@i
7. v : (A × B) List@i
8. ∀b:B. ((b ∈ reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];v)) ⇐⇒ (<a, b> ∈ v))@i
⊢ ∀b:B
    ((b ∈ if eqof(eq1) (fst(u)) a
      then insert(snd(u);reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];v))
      else reduce(λp,l. if eqof(eq1) (fst(p)) a then insert(snd(p);l) else l fi ;[];v)
      fi )
    ⇐⇒ (<a, b> ∈ [u / v]))

---

Latex:



1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)@i
4.  eq2  :  EqDecider(B)@i
5.  L  :  (A  \mtimes{}  B)  List@i
6.  a  :  A@i
\mvdash{}  \mforall{}b:B
        ((b  \mmember{}  reduce(\mlambda{}p,l.  if  eqof(eq1)  (fst(p))  a  then  insert(snd(p);l)  else  l  fi  ;[];L))  \mLeftarrow{}{}\mRightarrow{}  (<a,  b>  \mmember{}\000C  L))


By

((ListInd  (-2))  THEN  Reduce  0)

---

Home Index