---

Step * 3 2 1 1 2 of Lemma pairs-fpf_property


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]))
BY
{ (All (Unfold `eqof`)
   THEN ((((((ParallelLast THEN RWO "cons_member" 0) THENA Auto) THEN (RW (SweepDnC (RevHypC (-1))) 0)) THENA Auto)
          THEN (Thin (-1))
          THEN SplitOnConclITE)
         THENA Auto
         )
   THEN Try ((RWO "member-insert" 0 THENA Auto))
   THEN Auto
   THEN Try (ParallelLast)
   THEN Try ((OrRight THEN Auto))
   THEN SplitOrHyps
   THEN Auto) }

1
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@i
9. (fst(u)) = a ∈ A
10. b = (snd(u)) ∈ B@i
⊢ <a, b> = u ∈ (A × B)

---

Latex:



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


By

(All  (Unfold  `eqof`)
  THEN  ((((((ParallelLast  THEN  RWO  "cons\_member"  0)  THENA  Auto)
                    THEN  (RW  (SweepDnC  (RevHypC  (-1)))  0)
                    )
                  THENA  Auto
                  )
                THEN  (Thin  (-1))
                THEN  SplitOnConclITE)
              THENA  Auto
              )
  THEN  Try  ((RWO  "member-insert"  0  THENA  Auto))
  THEN  Auto
  THEN  Try  (ParallelLast)
  THEN  Try  ((OrRight  THEN  Auto))
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index