---

Step * 1 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
⊢ ((λ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)
BY
{ TACTIC:(Reduce 0 THEN ((GenConclAtAddrType ⌜B + Top⌝ [3; 1])⋅ THENA Auto) THEN D -2 THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. L1 : (A ⟶ (B + Top)) List
4. L2 : (A ⟶ (B + Top)) List
5. x : A
6. x1 : B@i
7. 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 ⋅ )
= (inl x1)
∈ (B + Top)
⊢ accumulate (with value v and list item f):
   case v of inl(z) => v | inr(z) => f x
  over list:
    L2
  with starting value:
   inl x1)
= (inl x1)
∈ (B + Top)

2
1. A : Type
2. B : Type
3. L1 : (A ⟶ (B + Top)) List
4. L2 : (A ⟶ (B + Top)) List
5. x : A
6. y : Top@i
7. 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 ⋅ )
= (inr y )
∈ (B + Top)
⊢ 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 y )
= 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 ⋅ )
∈ (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{}  ((\mlambda{}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  \mcdot{}  ))) 
      x)
=  ((\mlambda{}x.accumulate  (with  value  v  and  list  item  f):
                case  v  of  inl(z)  =>  v  |  inr(z)  =>  f  x
              over  list:
                  [\mlambda{}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  \mcdot{}  );
                    \mlambda{}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  \mcdot{}  )]
              with  starting  value:
                inr  \mcdot{}  )) 
      x)


By

---

Latex:
TACTIC:(Reduce  0  THEN  ((GenConclAtAddrType  \mkleeneopen{}B  +  Top\mkleeneclose{}  [3;  1])\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)

---

Home Index