---

Step * 1 of Lemma sq-decider-list-deq

.....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
BY
{ ((RWO "fun_exp_unroll_1" (-3) THENA Auto) THEN Reduce (-3)) }

1
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. (eval v = x 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,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 
                                                ⊥ 
                                                as' 
                                                bs') otherwise if v = Ax then ff otherwise ⊥)) 
                L) otherwise if v = Ax then λL.null(L) otherwise ⊥ 
    y)↓
9. z : Base
10. list-deq(eq) x y ~ inl z
⊢ x ~ y

---

Latex:

---

Latex:
.....eq  aux..... 
1.  eq  :  Base
2.  sq-decider(eq)
3.  j  :  \mBbbZ{}
4.  0  <  j
5.  \mforall{}x,y:Base.
          ((\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                      if  v  is  a  pair  then  let  a,as'  =  v 
                                                                              in  \mlambda{}L.(fix((\mlambda{}list$_{ind@0}$,L.  eval  v  =  L\000C  in
                                                                                                                                  if  v  is  a  pair  then  let  b,bs'  =  v 
                                                                                                                                                                          in  (eq  a  b)
                                                                                                                                                                                \mwedge{}\msubb{}  (list\mbackslash{}ff2\000C4_{ind}$ 
                                                                                                                                                                                        as' 
                                                                                                                                                                                        bs')
                                                                                                                                  otherwise  if  v  =  Ax  then  ff
                                                                                                                                                      otherwise  \mbot{})) 
                                                                                            L)  otherwise  if  v  =  Ax  then  \mlambda{}L.null(L)  otherwise  \mbot{}\^{}j  -\000C  1 
              \mbot{} 
              x 
              y)\mdownarrow{}
          {}\mRightarrow{}  (\mforall{}z:Base.  ((list-deq(eq)  x  y  \msim{}  inl  z)  {}\mRightarrow{}  (Ax  \mmember{}  x  \msim{}  y))))
6.  x  :  Base
7.  y  :  Base
8.  (\mlambda{}list$_{ind}$,L.  eval  v  =  L  in
                                if  v  is  a  pair
                                then  let  a,as'  =  v 
                                          in  \mlambda{}L.(fix((\mlambda{}list$_{ind@0}$,L.  eval  v  =  L  in
                                                                                              if  v  is  a  pair  then  let  b,bs'  =  v 
                                                                                                                                      in  (eq  a  b)  \mwedge{}\msubb{}  (list$_\mbackslash{}ff\000C7bind}$  as'  bs')
                                                                                              otherwise  if  v  =  Ax  then  ff  otherwise  \mbot{})) 
                                                        L)  otherwise  if  v  =  Ax  then  \mlambda{}L.null(L)  otherwise  \mbot{}\^{}j 
        \mbot{} 
        x 
        y)\mdownarrow{}
9.  z  :  Base
10.  list-deq(eq)  x  y  \msim{}  inl  z
\mvdash{}  x  \msim{}  y


By

---

Latex:
((RWO  "fun\_exp\_unroll\_1"  (-3)  THENA  Auto)  THEN  Reduce  (-3))

---

Home Index