---

Step * of Lemma bl-exists-append

∀[L1,L2,P:Top].  ((∃x∈L1 @ L2.P[x])_b ~ (∃x∈L1.P[x])_b ∨b(∃x∈L2.P[x])_b)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``bl-exists`` 0
   THEN (RWO "reduce-append" 0 THENA Auto)
   THEN (GenConclAtAddrType ⌜Top⌝ [2;2]⋅ THENA Auto)
   THEN Thin (-1)
   THEN ThinVar `L2'
   THEN RepUR ``reduce list_ind`` 0
   THEN SqequalSqle
   THEN OneFixpointLeast
   THEN RepeatFor 3 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((RepUR ``bor ifthenelse`` 0 THEN Strictness THEN Auto)))
   THEN (RWO "fun_exp_unroll" 0 THENA Auto)
   THEN AutoSplit) }

1
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L1,P,v:Top.
     (λlist_ind,L. eval v@0 = L in
                   if v@0 is a pair then let a,as' = v@0 
                                         in P[a] ∨b(list_ind as') otherwise if v@0 = Ax then v otherwise ⊥^j - 1 
      ⊥ 
      L1 ≤ (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 ⊥)) 
            L1)
      ∨bv)
5. L1 : Top
6. P : Top
7. v : Top
⊢ eval v@0 = L1 in
  if v@0 is a pair then let a,as' = v@0 
                        in P[a]
                           ∨b(λlist_ind,L. eval v@0 = L in
                                           if v@0 is a pair then let a,as' = v@0 
                                                                 in P[a] ∨b(list_ind as')
                                           otherwise if v@0 = Ax then v otherwise ⊥^j - 1 
                              ⊥ 
                              as') otherwise if v@0 = Ax then v otherwise ⊥ ≤ (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 
                                                                               L1)
  ∨bv

2
1. j : ℤ
2. j ≠ 0
3. 0 < j
4. ∀L1,P,v:Top.
     ((λ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 
       ⊥ 
       L1)
      ∨bv ≤ fix((λlist_ind,L. eval v@0 = L in
                              if v@0 is a pair then let a,as' = v@0 
                                                    in P[a] ∨b(list_ind as') otherwise if v@0 = Ax then v otherwise ⊥)) 
            L1)
5. L1 : Top
6. P : Top
7. v : Top
⊢ eval v = L1 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 ⊥
  ∨bv ≤ fix((λlist_ind,L. eval v@0 = L in
                          if v@0 is a pair then let a,as' = v@0 
                                                in P[a] ∨b(list_ind as') otherwise if v@0 = Ax then v otherwise ⊥)) 
        L1

---

Latex:

---

Latex:
\mforall{}[L1,L2,P:Top].    ((\mexists{}x\mmember{}L1  @  L2.P[x])\_b  \msim{}  (\mexists{}x\mmember{}L1.P[x])\_b  \mvee{}\msubb{}(\mexists{}x\mmember{}L2.P[x])\_b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``bl-exists``  0
  THEN  (RWO  "reduce-append"  0  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}Top\mkleeneclose{}  [2;2]\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  ThinVar  `L2'
  THEN  RepUR  ``reduce  list\_ind``  0
  THEN  SqequalSqle
  THEN  OneFixpointLeast
  THEN  RepeatFor  3  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((RepUR  ``bor  ifthenelse``  0  THEN  Strictness  THEN  Auto)))
  THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index