---

Step * of Lemma cWO-induction-extract-sqequal

λf.fix((λF,t. (f t F))) ~ TERMOF{cWO-induction_1-ext:o, \\v:l, i:l}
BY
{ (RW (SubC (TagC (mk_tag_term 10))) 0
   THEN Unfold `bar_recursion` 0
   THEN Reduce 0
   THEN EqCD
   THEN RW (SubC (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN RepeatFor 2 (EqCD)
   THEN Try (Trivial)) }

1
1. f : Base
2. t : Base
⊢ fix((λF,t. (f t F))) ~ λs1.(fix((λbar_recursion,n,s. case if (0) < (n)
                                                           then if s (n - 1)
                                                                then inr (λp.let _,_ = p 
                                                                             in Ax) 
                                                                else inl <Ax, Ax>
                                                                fi 
                                                           else (inr (λp.let _,_ = p 
                                                                         in Ax) )
                                                   of inl(r) =>
                                                   λa.let _,_ = r 
                                                      in Ax
                                                   | inr(r) =>
                                                   λa.(f a 
                                                       (λs1.(bar_recursion (n + 1) (λm.if m=n  then inl a  else (s m)) 
                                                             s1))))) 
                          1 
                          (λm.if m=0  then inl t  else if (m) < (0)  then 0 m  else ⊥) 
                          s1)

---

Latex:

---

Latex:
\mlambda{}f.fix((\mlambda{}F,t.  (f  t  F)))  \msim{}  TERMOF\{cWO-induction\_1-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}


By

---

Latex:
(RW  (SubC  (TagC  (mk\_tag\_term  10)))  0
  THEN  Unfold  `bar\_recursion`  0
  THEN  Reduce  0
  THEN  EqCD
  THEN  RW  (SubC  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (Trivial))

---

Home Index