---

Step * 1 1 1 of Lemma term-accum-induction


1. opr : Type
2. P : Type
3. R : P ⟶ term(opr) ⟶ ℙ
4. Q : P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P
5. f : opr
6. p : P
7. u : varname() List × term(opr)
8. v : (varname() List × term(opr)) List
9. g : ∀bt:{bt:varname() List × term(opr)| (bt ∈ [u / v])} . ∀p:P.  R[p;snd(bt)]
10. X : (varname() List × term(opr)) List
11. LL : (t:term(opr) × p:P × R[p;t]) List
12. ||LL|| = ||X|| ∈ ℤ
13. ∀i:ℕ||LL||. ((fst(LL[i])) = (snd(X[i])) ∈ term(opr))
14. ∀i:ℕ||LL||. ((fst(snd(LL[i]))) = Q[p;f;fst(X[i]);firstn(i;LL)] ∈ P)
15. i : ℕ||LL|| + 1
16. ¬i < ||LL||
⊢ Q[p;f;fst(u);LL] = Q[p;f;fst(u);firstn(i;LL @ [<snd(u), Q[p;f;fst(u);LL], g u Q[p;f;fst(u);LL]>])] ∈ P
BY
{ (EqCDA THEN ((RWO "firstn-append" 0 THENM OReduce 0) THENA Auto) THEN Subst' i ~ ||LL|| 0 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  P  :  Type
3.  R  :  P  {}\mrightarrow{}  term(opr)  {}\mrightarrow{}  \mBbbP{}
4.  Q  :  P  {}\mrightarrow{}  opr  {}\mrightarrow{}  (varname()  List)  {}\mrightarrow{}  ((t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List)  {}\mrightarrow{}  P
5.  f  :  opr
6.  p  :  P
7.  u  :  varname()  List  \mtimes{}  term(opr)
8.  v  :  (varname()  List  \mtimes{}  term(opr))  List
9.  g  :  \mforall{}bt:\{bt:varname()  List  \mtimes{}  term(opr)|  (bt  \mmember{}  [u  /  v])\}  .  \mforall{}p:P.    R[p;snd(bt)]
10.  X  :  (varname()  List  \mtimes{}  term(opr))  List
11.  LL  :  (t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List
12.  ||LL||  =  ||X||
13.  \mforall{}i:\mBbbN{}||LL||.  ((fst(LL[i]))  =  (snd(X[i])))
14.  \mforall{}i:\mBbbN{}||LL||.  ((fst(snd(LL[i])))  =  Q[p;f;fst(X[i]);firstn(i;LL)])
15.  i  :  \mBbbN{}||LL||  +  1
16.  \mneg{}i  <  ||LL||
\mvdash{}  Q[p;f;fst(u);LL]  =  Q[p;f;fst(u);firstn(i;LL  @  [<snd(u),  Q[p;f;fst(u);LL],  g  u  Q[p;f;fst(u);LL]>])]


By

---

Latex:
(EqCDA  THEN  ((RWO  "firstn-append"  0  THENM  OReduce  0)  THENA  Auto)  THEN  Subst'  i  \msim{}  ||LL||  0  THEN  Auto)

---

Home Index