---

Step * 1 of Lemma bbar-recursion_wf


1. T : Type
2. R : (T List) ⟶ 𝔹
3. A : (T List) ⟶ ℙ
4. b : ∀s:{s:T List| ↑R[s]} . A[s]
5. i : ∀s:{s:T List| ¬↑R[s]} . ((∀t:T. A[s @ [t]]) ⇒ A[s])
6. s : T List
7. ∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[s @ map(alpha;upto(n))]))
⊢ (λx.bbar-recursion(R;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
   THEN Try ((Fold `decidable` 0 THEN Auto))
   THEN RecUnfold `bbar-recursion` 0⋅
   THEN AutoSplit
   THEN Auto
   THEN RWO "append_assoc" 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  b  :  \mforall{}s:\{s:T  List|  \muparrow{}R[s]\}  .  A[s]
5.  i  :  \mforall{}s:\{s:T  List|  \mneg{}\muparrow{}R[s]\}  .  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s])
6.  s  :  T  List
7.  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  (\muparrow{}R[s  @  map(alpha;upto(n))]))
\mvdash{}  (\mlambda{}x.bbar-recursion(R;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'.(\muparrow{}(R  (s  @  s')))\mkleeneclose{}\mcdot{}\mcdot{}
  THEN  Reduce  0
  THEN  Try  (BackThruSomeHyp')
  THEN  All  Reduce
  THEN  Auto
  THEN  Try  ((Fold  `decidable`  0  THEN  Auto))
  THEN  RecUnfold  `bbar-recursion`  0\mcdot{}
  THEN  AutoSplit
  THEN  Auto
  THEN  RWO  "append\_assoc"  0
  THEN  Auto)\mcdot{}

---

Home Index