---

Step * of Lemma decidable__list-closed2-ext

∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T).  Dec(list-closed(T;L;f))
BY
{ Extract of Obid: decidable__list-closed2
  not unfolding  l-all-decider
  finishing with Auto
  normalizes to:
  
  λL,f,d. (l-all-decider() L 
           (λx.(l-all-decider() (f x) 
                (λz.letrec list_ind(L)=eval v = L in
                                       if v is a pair then let a,L = v 
                                                           in case list_ind L
                                                               of inl(%2) =>
                                                               if d z a
                                                               then inl <0, Ax, Ax>
                                                               else inl let i,%4,%5 = %2 in 
                                                                    <i + 1, Ax, Ax>
                                                               fi 
                                                               | inr(%2) =>
                                                               if d z a then inl <0, Ax, Ax> else inr (λ%.Ax)  fi 
                                       otherwise if v = Ax then inr (λ%.Ax)  otherwise fix((λx.x)) in
                     list_ind(L))))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}f:T  {}\mrightarrow{}  (T  List).  \mforall{}d:EqDecider(T).    Dec(list-closed(T;L;f))


By

---

Latex:
Extract  of  Obid:  decidable\_\_list-closed2
not  unfolding    l-all-decider
finishing  with  Auto
normalizes  to:

\mlambda{}L,f,d.  (l-all-decider()  L 
                  (\mlambda{}x.(l-all-decider()  (f  x) 
                            (\mlambda{}z.letrec  list$_{ind}$(L)=eval  v  =  L  in
                                                                        if  v  is  a  pair  then  let  a,L  =  v 
                                                                                                                in  case  list$_{ind}$  L
                                                                                                                        of  inl(\%2)  =>
                                                                                                                        if  d  z  a
                                                                                                                        then  inl  ɘ,  Ax,  Ax>
                                                                                                                        else  inl  let  i,\%4,\%5  =  \%2  in 
                                                                                                                                  <i  +  1,  Ax,  Ax>
                                                                                                                        fi 
                                                                                                                        |  inr(\%2)  =>
                                                                                                                        if  d  z  a
                                                                                                                        then  inl  ɘ,  Ax,  Ax>
                                                                                                                        else  inr  (\mlambda{}\%.Ax) 
                                                                                                                        fi 
                                                                        otherwise  if  v  =  Ax  then  inr  (\mlambda{}\%.Ax)    otherwise  fix((\mlambda{}x.x))  in
                                      list$_{ind}$(L)))))

---

Home Index