---

Step * 1 of Lemma accum_induction

.....subterm..... T:t
1:n
1. T : Type
2. Q : (T List) ⟶ ℙ
3. f : ⋂ys:T List. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
4. b : Q[[]]
5. L : T List
⊢ accumulate (with value p and list item y):
   f p y
  over list:
    L
  with starting value:
   b) ∈ Q[L]
BY
{ (MoveToConcl (-1) THEN InductionOnLength THEN (Decide ⌜↑null(L)⌝⋅ THENA Auto)) }

1
1. T : Type
2. Q : (T List) ⟶ ℙ
3. f : ⋂ys:T List. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
4. b : Q[[]]
5. n : ℕ
6. L : T List
7. ∀L1:T List
     (||L1|| < ||L|| ⇒ (accumulate (with value p and list item y): f p yover list:  L1with starting value: b) ∈ Q[L1]))
8. ↑null(L)
⊢ accumulate (with value p and list item y):
   f p y
  over list:
    L
  with starting value:
   b) ∈ Q[L]

2
1. T : Type
2. Q : (T List) ⟶ ℙ
3. f : ⋂ys:T List. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
4. b : Q[[]]
5. n : ℕ
6. L : T List
7. ∀L1:T List
     (||L1|| < ||L|| ⇒ (accumulate (with value p and list item y): f p yover list:  L1with starting value: b) ∈ Q[L1]))
8. ¬↑null(L)
⊢ accumulate (with value p and list item y):
   f p y
  over list:
    L
  with starting value:
   b) ∈ Q[L]

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  Q  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  f  :  \mcap{}ys:T  List.  (Q[ys]  {}\mRightarrow{}  (\mforall{}y:T.  Q[ys  @  [y]]))
4.  b  :  Q[[]]
5.  L  :  T  List
\mvdash{}  accumulate  (with  value  p  and  list  item  y):
      f  p  y
    over  list:
        L
    with  starting  value:
      b)  \mmember{}  Q[L]


By

---

Latex:
(MoveToConcl  (-1)  THEN  InductionOnLength  THEN  (Decide  \mkleeneopen{}\muparrow{}null(L)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index