---

Step * of Lemma bar-induction

∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
  ((∀s:T List. Dec(R[s]))
  ⇒ (∀s:T List. (R[s] ⇒ A[s]))
  ⇒ (∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s]))
  ⇒ (∀s:T List. ((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[s @ map(alpha;upto(n))])) ⇒ A[s])))
BY
{ (Auto
   THEN InstLemma `bar_induction` [⌜T⌝;⌜λn,s. R[map(s;upto(n))]⌝;⌜λn,s. A[map(s;upto(n))]⌝]⋅
   THEN All (RepUR ``so_apply``)
   THEN Auto)⋅ }

1
1. [T] : Type
2. [R] : (T List) ⟶ ℙ
3. [A] : (T List) ⟶ ℙ
4. ∀s:T List. Dec(R s)
5. ∀s:T List. ((R s) ⇒ (A s))
6. ∀s:T List. ((∀t:T. (A (s @ [t]))) ⇒ (A s))
7. s : T List
8. ∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (R (s @ map(alpha;upto(n)))))
9. n : ℕ
10. s1 : ℕn ⟶ T
11. ∀t:T. (A map(s1++t;upto(n + 1)))
⊢ A map(s1;upto(n))

2
1. [T] : Type
2. [R] : (T List) ⟶ ℙ
3. [A] : (T List) ⟶ ℙ
4. ∀s:T List. Dec(R s)
5. ∀s:T List. ((R s) ⇒ (A s))
6. ∀s:T List. ((∀t:T. (A (s @ [t]))) ⇒ (A s))
7. s : T List
8. ∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (R (s @ map(alpha;upto(n)))))
9. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R map(seq-append(n;m;s;alpha);upto(n + m))))) ⇒ (A map(s;upto(n))))
⊢ A s

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}s:T  List.  Dec(R[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  (R[s]  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  R[s  @  map(alpha;upto(n))]))  {}\mRightarrow{}  A[s])))


By

---

Latex:
(Auto
  THEN  InstLemma  `bar\_induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}n,s.  R[map(s;upto(n))]\mkleeneclose{};\mkleeneopen{}\mlambda{}n,s.  A[map(s;upto(n))]\mkleeneclose{}]\mcdot{}
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)\mcdot{}

---

Home Index