---

Step * of Lemma not-bl-exists-eq-bl-all

∀[L,P:Top].  (¬b(∃x∈L.P[x])_b ~ (∀x∈L.¬bP[x])_b)
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualTopToBase
   THEN SqequalSqle
   THEN RepUR ``bl-exists bl-all reduce list_ind`` 0
   THEN OneFixpointLeast
   THEN (Repeat (MoveToConcl (-2))
         THEN NatInd (-1)
         THEN Reduce 0
         THEN Strictness
         THEN UnivCD
         THEN Try (Complete (Auto))
         THEN (RWO "fun_exp_unroll_1" 0 THENA Auto)
         THEN Reduce 0
         THEN AssumeHasValue
         THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (ComputeSameException 200))))⋅) }

1
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (¬b(λlist_ind,L. eval v = L in
                      if v is a pair then let a,as' = v 
                                          in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1 
         ⊥ 
         L) ≤ fix((λlist_ind,L. eval v = L in
                                if v is a pair then let a,as' = v 
                                                    in (¬bP[a]) ∧b (list_ind as')
                                otherwise if v = Ax then tt otherwise ⊥)) 
              L)
4. P : Base@i
5. L : Base@i
6. (¬beval v = L in
      if v is a pair then let a,as' = v 
                          in P[a]
                             ∨b(λlist_ind,L. eval v = L in
                                             if v is a pair then let a,as' = v 
                                                                 in P[a] ∨b(list_ind as')
                                             otherwise if v = Ax then ff otherwise ⊥^j - 1 
                                ⊥ 
                                as') otherwise if v = Ax then ff otherwise ⊥)↓
7. eval v = L in
   if v is a pair then let a,as' = v 
                       in P[a]
                          ∨b(λlist_ind,L. eval v = L in
                                          if v is a pair then let a,as' = v 
                                                              in P[a] ∨b(list_ind as')
                                          otherwise if v = Ax then ff otherwise ⊥^j - 1 
                             ⊥ 
                             as') otherwise if v = Ax then ff otherwise ⊥ ∈ Top + Top
⊢ ¬beval v = L in
    if v is a pair then let a,as' = v 
                        in P[a]
                           ∨b(λlist_ind,L. eval v = L in
                                           if v is a pair then let a,as' = v 
                                                               in P[a] ∨b(list_ind as')
                                           otherwise if v = Ax then ff otherwise ⊥^j - 1 
                              ⊥ 
                              as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
                                                                                             if v is a pair
                                                                                             then let a,as' = v 
                                                                                                  in (¬bP[a])
                                                                                                     ∧b (list_ind as')
                                                                                             otherwise if v = Ax then tt
                                                                                                       otherwise ⊥)) 
                                                                           L

2
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (¬b(λlist_ind,L. eval v = L in
                      if v is a pair then let a,as' = v 
                                          in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1 
         ⊥ 
         L) ≤ fix((λlist_ind,L. eval v = L in
                                if v is a pair then let a,as' = v 
                                                    in (¬bP[a]) ∧b (list_ind as')
                                otherwise if v = Ax then tt otherwise ⊥)) 
              L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
                     if v is a pair then let a,as' = v 
                                         in P[a]
                                            ∨b(λlist_ind,L. eval v = L in
                                                            if v is a pair then let a,as' = v 
                                                                                in P[a] ∨b(list_ind as')
                                                            otherwise if v = Ax then ff otherwise ⊥^j - 1 
                                               ⊥ 
                                               as') otherwise if v = Ax then ff otherwise ⊥
 of inl() =>
 ff
 | inr() =>
 tt)
7. eval v = L in
   if v is a pair then let a,as' = v 
                       in P[a]
                          ∨b(λlist_ind,L. eval v = L in
                                          if v is a pair then let a,as' = v 
                                                              in P[a] ∨b(list_ind as')
                                          otherwise if v = Ax then ff otherwise ⊥^j - 1 
                             ⊥ 
                             as') otherwise if v = Ax then ff otherwise ⊥ ∈ Top + Top
⊢ ¬beval v = L in
    if v is a pair then let a,as' = v 
                        in P[a]
                           ∨b(λlist_ind,L. eval v = L in
                                           if v is a pair then let a,as' = v 
                                                               in P[a] ∨b(list_ind as')
                                           otherwise if v = Ax then ff otherwise ⊥^j - 1 
                              ⊥ 
                              as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
                                                                                             if v is a pair
                                                                                             then let a,as' = v 
                                                                                                  in (¬bP[a])
                                                                                                     ∧b (list_ind as')
                                                                                             otherwise if v = Ax then tt
                                                                                                       otherwise ⊥)) 
                                                                           L

3
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (¬b(λlist_ind,L. eval v = L in
                      if v is a pair then let a,as' = v 
                                          in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥^j - 1 
         ⊥ 
         L) ≤ fix((λlist_ind,L. eval v = L in
                                if v is a pair then let a,as' = v 
                                                    in (¬bP[a]) ∧b (list_ind as')
                                otherwise if v = Ax then tt otherwise ⊥)) 
              L)
4. P : Base@i
5. L : Base@i
6. is-exception(case eval v = L in
                     if v is a pair then let a,as' = v 
                                         in P[a]
                                            ∨b(λlist_ind,L. eval v = L in
                                                            if v is a pair then let a,as' = v 
                                                                                in P[a] ∨b(list_ind as')
                                                            otherwise if v = Ax then ff otherwise ⊥^j - 1 
                                               ⊥ 
                                               as') otherwise if v = Ax then ff otherwise ⊥
 of inl() =>
 ff
 | inr() =>
 tt)
7. is-exception(eval v = L in
                if v is a pair then let a,as' = v 
                                    in P[a]
                                       ∨b(λlist_ind,L. eval v = L in
                                                       if v is a pair then let a,as' = v 
                                                                           in P[a] ∨b(list_ind as')
                                                       otherwise if v = Ax then ff otherwise ⊥^j - 1 
                                          ⊥ 
                                          as') otherwise if v = Ax then ff otherwise ⊥)
⊢ ¬beval v = L in
    if v is a pair then let a,as' = v 
                        in P[a]
                           ∨b(λlist_ind,L. eval v = L in
                                           if v is a pair then let a,as' = v 
                                                               in P[a] ∨b(list_ind as')
                                           otherwise if v = Ax then ff otherwise ⊥^j - 1 
                              ⊥ 
                              as') otherwise if v = Ax then ff otherwise ⊥ ≤ fix((λlist_ind,L. eval v = L in
                                                                                             if v is a pair
                                                                                             then let a,as' = v 
                                                                                                  in (¬bP[a])
                                                                                                     ∧b (list_ind as')
                                                                                             otherwise if v = Ax then tt
                                                                                                       otherwise ⊥)) 
                                                                           L

4
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (λlist_ind,L. eval v = L in
                   if v is a pair then let a,as' = v 
                                       in (¬bP[a]) ∧b (list_ind as') otherwise if v = Ax then tt otherwise ⊥^j - 1 
      ⊥ 
      L ≤ ¬b(fix((λlist_ind,L. eval v = L in
                               if v is a pair then let a,as' = v 
                                                   in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥)) 
             L))
4. P : Base@i
5. L : Base@i
6. (if L is a pair then let a,as' = L 
                        in (¬bP[a])
                           ∧b (λlist_ind,L. eval v = L in
                                            if v is a pair then let a,as' = v 
                                                                in (¬bP[a]) ∧b (list_ind as')
                                            otherwise if v = Ax then tt otherwise ⊥^j - 1 
                               ⊥ 
                               as') otherwise if L = Ax then tt otherwise ⊥)↓
7. (L)↓
⊢ if L is a pair then let a,as' = L 
                      in (¬bP[a])
                         ∧b (λlist_ind,L. eval v = L in
                                          if v is a pair then let a,as' = v 
                                                              in (¬bP[a]) ∧b (list_ind as')
                                          otherwise if v = Ax then tt otherwise ⊥^j - 1 
                             ⊥ 
                             as') otherwise if L = Ax then tt otherwise ⊥ ≤ ¬b(fix((λlist_ind,L. eval v = L in
                                                                                                 if v is a pair
                                                                                                 then let a,as' = v 
                                                                                                      in P[a]
                                                                                                         ∨b(list_ind 
                                                                                                            as')
                                                                                                 otherwise if v = Ax
                                                                                                           then ff
                                                                                                           otherwise ⊥))\000C 
                                                                               L)

5
1. j : ℤ
2. 0 < j
3. ∀P,L:Base.
     (λlist_ind,L. eval v = L in
                   if v is a pair then let a,as' = v 
                                       in (¬bP[a]) ∧b (list_ind as') otherwise if v = Ax then tt otherwise ⊥^j - 1 
      ⊥ 
      L ≤ ¬b(fix((λlist_ind,L. eval v = L in
                               if v is a pair then let a,as' = v 
                                                   in P[a] ∨b(list_ind as') otherwise if v = Ax then ff otherwise ⊥)) 
             L))
4. P : Base@i
5. L : Base@i
6. is-exception(eval v = L in
                if v is a pair then let a,as' = v 
                                    in (¬bP[a])
                                       ∧b (λlist_ind,L. eval v = L in
                                                        if v is a pair then let a,as' = v 
                                                                            in (¬bP[a]) ∧b (list_ind as')
                                                        otherwise if v = Ax then tt otherwise ⊥^j - 1 
                                           ⊥ 
                                           as') otherwise if v = Ax then tt otherwise ⊥)
7. (L)↓
⊢ eval v = L in
  if v is a pair then let a,as' = v 
                      in (¬bP[a])
                         ∧b (λlist_ind,L. eval v = L in
                                          if v is a pair then let a,as' = v 
                                                              in (¬bP[a]) ∧b (list_ind as')
                                          otherwise if v = Ax then tt otherwise ⊥^j - 1 
                             ⊥ 
                             as') otherwise if v = Ax then tt otherwise ⊥ ≤ ¬b(fix((λlist_ind,L. eval v = L in
                                                                                                 if v is a pair
                                                                                                 then let a,as' = v 
                                                                                                      in P[a]
                                                                                                         ∨b(list_ind 
                                                                                                            as')
                                                                                                 otherwise if v = Ax
                                                                                                           then ff
                                                                                                           otherwise ⊥))\000C 
                                                                               L)

---

Latex:

---

Latex:
\mforall{}[L,P:Top].    (\mneg{}\msubb{}(\mexists{}x\mmember{}L.P[x])\_b  \msim{}  (\mforall{}x\mmember{}L.\mneg{}\msubb{}P[x])\_b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  SqequalSqle
  THEN  RepUR  ``bl-exists  bl-all  reduce  list\_ind``  0
  THEN  OneFixpointLeast
  THEN  (Repeat  (MoveToConcl  (-2))
              THEN  NatInd  (-1)
              THEN  Reduce  0
              THEN  Strictness
              THEN  UnivCD
              THEN  Try  (Complete  (Auto))
              THEN  (RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)
              THEN  Reduce  0
              THEN  AssumeHasValue
              THEN  (HasValueD  (-1)  ORELSE  (ExceptionCases  (-1)  THEN  Try  (ComputeSameException  200))))\mcdot{})

---

Home Index