---

Step * 1 2 of Lemma bar-recursion_wf


1. T : Type
2. R : (T List) ⟶ ℙ
3. A : (T List) ⟶ ℙ
4. d : ∀s:T List. Dec(R[s])
5. b : ∀s:T List. (R[s] ⇒ A[s])
6. i : ∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s])
7. s : T List
8. ∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[s @ map(alpha;upto(n))])@i
⊢ (λx.bar-recursion(d;b;i;s @ x)) [] ∈ (λx.A[s @ x]) []
BY
{ (All (Unfold `so_apply`)⋅
   THEN BarInduction ⌜T⌝ ⌜λs'.(R (s @ s'))⌝⋅⋅
   THEN Reduce 0
   THEN Try (BackThruSomeHyp')
   THEN All Reduce
   THEN Auto) }

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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  d  :  \mforall{}s:T  List.  Dec(R[s])
5.  b  :  \mforall{}s:T  List.  (R[s]  {}\mRightarrow{}  A[s])
6.  i  :  \mforall{}s:T  List.  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s])
7.  s  :  T  List
8.  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  R[s  @  map(alpha;upto(n))])@i
\mvdash{}  (\mlambda{}x.bar-recursion(d;b;i;s  @  x))  []  \mmember{}  (\mlambda{}x.A[s  @  x])  []


By

---

Latex:
(All  (Unfold  `so\_apply`)\mcdot{}
  THEN  BarInduction  \mkleeneopen{}T\mkleeneclose{}  \mkleeneopen{}\mlambda{}s'.(R  (s  @  s'))\mkleeneclose{}\mcdot{}\mcdot{}
  THEN  Reduce  0
  THEN  Try  (BackThruSomeHyp')
  THEN  All  Reduce
  THEN  Auto)

---

Home Index