---

Step * 2 1 of Lemma fpf-join-assoc


1. A : Type
2. B : A ⟶ Type
3. eq : EqDecider(A)
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ⟶ B[a]
6. d1 : A List
7. g1 : a:{a:A| (a ∈ d1)}  ⟶ B[a]
8. d2 : A List
9. h1 : a:{a:A| (a ∈ d2)}  ⟶ B[a]
10. x : {a:A| (a ∈ d @ filter(λa.(¬ba ∈b d);d1 @ filter(λa.(¬ba ∈b d1);d2)))} 
⊢ if x ∈b d then f1 x
if x ∈b d1 then g1 x
else h1 x
fi 
= if x ∈b d @ filter(λa.(¬ba ∈b d);d1) then if x ∈b d then f1 x else g1 x fi  else h1 x fi 
∈ B[x]
BY
{ (D -1
   THEN (RWW "member_append member_filter" (-1) THENA Auto)
   THEN Reduce -1
   THEN (RWO "deq-member-append" 0 THENA Auto)
   THEN AutoSplit
   THEN D -1
   THEN Try (Trivial)
   THEN D -1
   THEN D -2
   THEN (RW assert_pushdownC (-2) THENA Auto)
   THEN RepeatFor 2 (AutoSplit)) }

1
1. A : Type
2. B : A ⟶ Type
3. eq : EqDecider(A)
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ⟶ B[a]
6. d1 : A List
7. g1 : a:{a:A| (a ∈ d1)}  ⟶ B[a]
8. d2 : A List
9. h1 : a:{a:A| (a ∈ d2)}  ⟶ B[a]
10. x : A
11. ¬(x ∈ filter(λa.(¬ba ∈b d);d1))
12. ¬(x ∈ d)
13. (x ∈ d1)
14. True
15. (x ∈ d1)
⊢ (g1 x) = (h1 x) ∈ B[x]

2
1. A : Type
2. B : A ⟶ Type
3. eq : EqDecider(A)
4. d : A List
5. f1 : a:{a:A| (a ∈ d)}  ⟶ B[a]
6. d1 : A List
7. g1 : a:{a:A| (a ∈ d1)}  ⟶ B[a]
8. d2 : A List
9. h1 : a:{a:A| (a ∈ d2)}  ⟶ B[a]
10. x : A
11. ¬(x ∈ d1)
12. ¬(x ∈ d)
13. (x ∈ d2) ∧ (¬(x ∈ d1))
14. True
15. (x ∈ filter(λa.(¬ba ∈b d);d1))
⊢ (h1 x) = (g1 x) ∈ B[x]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  eq  :  EqDecider(A)
4.  d  :  A  List
5.  f1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a]
6.  d1  :  A  List
7.  g1  :  a:\{a:A|  (a  \mmember{}  d1)\}    {}\mrightarrow{}  B[a]
8.  d2  :  A  List
9.  h1  :  a:\{a:A|  (a  \mmember{}  d2)\}    {}\mrightarrow{}  B[a]
10.  x  :  \{a:A|  (a  \mmember{}  d  @  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}\msubb{}  d);d1  @  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}\msubb{}  d1);d2)))\} 
\mvdash{}  if  x  \mmember{}\msubb{}  d  then  f1  x
if  x  \mmember{}\msubb{}  d1  then  g1  x
else  h1  x
fi 
=  if  x  \mmember{}\msubb{}  d  @  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}\msubb{}  d);d1)  then  if  x  \mmember{}\msubb{}  d  then  f1  x  else  g1  x  fi    else  h1  x  fi 


By

---

Latex:
(D  -1
  THEN  (RWW  "member\_append  member\_filter"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  (RWO  "deq-member-append"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  D  -1
  THEN  Try  (Trivial)
  THEN  D  -1
  THEN  D  -2
  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index