Step * 1 2 2 of Lemma accum_induction


1. Type
2. (T List) ⟶ ℙ
3. : ⋂ys:T List. (Q[ys]  (∀y:T. Q[ys [y]]))
4. Q[[]]
5. : ℕ
6. List
7. ∀L1:T List
     (||L1|| < ||L||  (accumulate (with value and list item y): yover list:  L1with starting value: b) ∈ Q[L1]))
8. ¬↑null(L)
⊢ accumulate (with value and list item y):
   y
  over list:
    firstn(||L|| 1;L) [last(L)]
  with starting value:
   b) ∈ Q[firstn(||L|| 1;L) [last(L)]]
BY
TACTIC:(RWO "list_accum_append" THENA Auto) }

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


Latex:


Latex:

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.  n  :  \mBbbN{}
6.  L  :  T  List
7.  \mforall{}L1:T  List
          (||L1||  <  ||L||
          {}\mRightarrow{}  (accumulate  (with  value  p  and  list  item  y):
                    f  p  y
                  over  list:
                      L1
                  with  starting  value:
                    b)  \mmember{}  Q[L1]))
8.  \mneg{}\muparrow{}null(L)
\mvdash{}  accumulate  (with  value  p  and  list  item  y):
      f  p  y
    over  list:
        firstn(||L||  -  1;L)  @  [last(L)]
    with  starting  value:
      b)  \mmember{}  Q[firstn(||L||  -  1;L)  @  [last(L)]]


By


Latex:
TACTIC:(RWO  "list\_accum\_append"  0  THENA  Auto)




Home Index