---

Step * 1 of Lemma p-first-append


1. A : Type
2. B : Type
3. L1 : (A ⟶ (B + Top)) List
4. L2 : (A ⟶ (B + Top)) List
5. x : A
⊢ (p-first(L1 @ L2) x) = (p-first([p-first(L1); p-first(L2)]) x) ∈ (B + Top)
BY
{ TACTIC:(Unfold `p-first` 0 THEN (RWO "list_accum_append" 0 THENA Auto)) }

1
1. A : Type
2. B : Type
3. L1 : (A ⟶ (B + Top)) List
4. L2 : (A ⟶ (B + Top)) List
5. x : A
⊢ ((λx.accumulate (with value v and list item f):
        case v of inl(z) => v | inr(z) => f x
       over list:
         L2
       with starting value:
        accumulate (with value v and list item f):
         case v of inl(z) => v | inr(z) => f x
        over list:
          L1
        with starting value:
         inr ⋅ ))) 
   x)
= ((λx.accumulate (with value v and list item f):
        case v of inl(z) => v | inr(z) => f x
       over list:
         [λx.accumulate (with value v and list item f):
              case v of inl(z) => v | inr(z) => f x
             over list:
               L1
             with starting value:
              inr ⋅ );
          λx.accumulate (with value v and list item f):
              case v of inl(z) => v | inr(z) => f x
             over list:
               L2
             with starting value:
              inr ⋅ )]
       with starting value:
        inr ⋅ )) 
   x)
∈ (B + Top)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  L1  :  (A  {}\mrightarrow{}  (B  +  Top))  List
4.  L2  :  (A  {}\mrightarrow{}  (B  +  Top))  List
5.  x  :  A
\mvdash{}  (p-first(L1  @  L2)  x)  =  (p-first([p-first(L1);  p-first(L2)])  x)


By

---

Latex:
TACTIC:(Unfold  `p-first`  0  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto))

---

Home Index