---

Step * of Lemma sq-decider-list-deq

∀[eq:Base]. sq-decider(list-deq(eq)) supposing sq-decider(eq)
BY
{ (Auto
   THEN RepeatFor 3 ((D 0⋅ THENA Auto))
   THEN ExRepD
   THEN (Assert ⌜(list-deq(eq) x y)↓⌝⋅ THENA (HypSubst' (-1) 0 THEN Auto))
   THEN RepUR ``list-deq list_ind`` -1
   THEN Compactness (-1)
   THEN UseWitness ⌜Ax⌝⋅
   THEN Thin (-3)
   THEN RepeatFor 2 (MoveToConcl (-3))
   THEN MoveToConcl (-1)
   THEN RepeatFor 2 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Strictness
   THEN (UnivCD THENA Auto)
   THEN BotDiv
   THEN MemCD) }

1
.....eq aux..... 
1. eq : Base
2. sq-decider(eq)
3. j : ℤ
4. 0 < j
5. ∀x,y:Base.
     ((λlist_ind,L. eval v = L in
                    if v is a pair then let a,as' = v 
                                        in λL.(fix((λlist_ind@0,L. eval v = L in
                                                                   if v is a pair then let b,bs' = v 
                                                                                       in (eq a b) ∧b (list_ind as' bs')
                                                                   otherwise if v = Ax then ff otherwise ⊥)) 
                                               L) otherwise if v = Ax then λL.null(L) otherwise ⊥^j - 1 
       ⊥ 
       x 
       y)↓
     ⇒ (∀z:Base. ((list-deq(eq) x y ~ inl z) ⇒ (Ax ∈ x ~ y))))
6. x : Base
7. y : Base
8. (λlist_ind,L. eval v = L in
                 if v is a pair then let a,as' = v 
                                     in λL.(fix((λlist_ind@0,L. eval v = L in
                                                                if v is a pair then let b,bs' = v 
                                                                                    in (eq a b) ∧b (list_ind as' bs')
                                                                otherwise if v = Ax then ff otherwise ⊥)) 
                                            L) otherwise if v = Ax then λL.null(L) otherwise ⊥^j 
    ⊥ 
    x 
    y)↓
9. z : Base
10. list-deq(eq) x y ~ inl z
⊢ x ~ y

---

Latex:

---

Latex:
\mforall{}[eq:Base].  sq-decider(list-deq(eq))  supposing  sq-decider(eq)


By

---

Latex:
(Auto
  THEN  RepeatFor  3  ((D  0\mcdot{}  THENA  Auto))
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}(list-deq(eq)  x  y)\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  (HypSubst'  (-1)  0  THEN  Auto))
  THEN  RepUR  ``list-deq  list\_ind``  -1
  THEN  Compactness  (-1)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  Thin  (-3)
  THEN  RepeatFor  2  (MoveToConcl  (-3))
  THEN  MoveToConcl  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Strictness
  THEN  (UnivCD  THENA  Auto)
  THEN  BotDiv
  THEN  MemCD)

---

Home Index