---

Step * of Lemma b-almost-full-intersection

No Annotations
∀R,T:ℕ ⟶ ℕ ⟶ ℙ.  (b-almost-full(n,m.R[n;m]) ⇒ b-almost-full(n,m.T[n;m]) ⇒ ⇃(∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m])))
BY
{ (Auto
   THEN (InstLemma `monotone-bar-induction-strict3`
          [⌜λ2l a.baf-bar(n,m.R[n;m];n,m.T[n;m];l;a)⌝
          ; ⌜λ2l a.∀s:StrictInc
                     ∃n:ℕ. (baf-bar(n,m.R[n;m];n,m.T[n;m];l + 1;a.s n@l) ∨ (∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m])))⌝
          ]⋅
         THENW Auto
         )
   ) }

1
.....antecedent..... 
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
⊢ ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
    (baf-bar(n,m.R[n;m];n,m.T[n;m];n;s)
    ⇒ (∀m:ℕ. (strictly-increasing-seq(n + 1;s.m@n) ⇒ baf-bar(n,m.R[n;m];n,m.T[n;m];n + 1;s.m@n))))

2
.....antecedent..... 
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
⊢ ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
    (baf-bar(n,m.R[n;m];n,m.T[n;m];n;s)
    ⇒ ⇃(∀s@0:StrictInc
           ∃n@0:ℕ. (baf-bar(n,m.R[n;m];n,m.T[n;m];n + 1;s.s@0 n@0@n) ∨ (∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m])))))

3
.....antecedent..... 
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
⊢ ∀n:ℕ. ∀s:{s:ℕn ⟶ ℕ| strictly-increasing-seq(n;s)} .
    ((∀m:ℕ
        (strictly-increasing-seq(n + 1;s.m@n)
        ⇒ ⇃(∀s@0:StrictInc
               ∃n@0:ℕ
                (baf-bar(n,m.R[n;m];n,m.T[n;m];(n + 1) + 1;s.m@n.s@0 n@0@n + 1)
                ∨ (∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m]))))))
    ⇒ ⇃(∀s@0:StrictInc
           ∃n@0:ℕ. (baf-bar(n,m.R[n;m];n,m.T[n;m];n + 1;s.s@0 n@0@n) ∨ (∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m])))))

4
.....antecedent..... 
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
⊢ ∀alpha:StrictInc. ⇃(∃m:ℕ. baf-bar(n,m.R[n;m];n,m.T[n;m];m;alpha))

5
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. T : ℕ ⟶ ℕ ⟶ ℙ
3. b-almost-full(n,m.R[n;m])
4. b-almost-full(n,m.T[n;m])
5. ⇃(∀s:StrictInc. ∃n:ℕ. (baf-bar(n,m.R[n;m];n,m.T[n;m];0 + 1;λx.⊥.s n@0) ∨ (∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m]))))
⊢ ⇃(∃n:ℕ. ∃m:{n + 1...}. (R[n;m] ∧ T[n;m]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}R,T:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
    (b-almost-full(n,m.R[n;m])
    {}\mRightarrow{}  b-almost-full(n,m.T[n;m])
    {}\mRightarrow{}  \00D9(\mexists{}n:\mBbbN{}.  \mexists{}m:\{n  +  1...\}.  (R[n;m]  \mwedge{}  T[n;m])))


By

---

Latex:
(Auto
  THEN  (InstLemma  `monotone-bar-induction-strict3`
                [\mkleeneopen{}\mlambda{}\msubtwo{}l  a.baf-bar(n,m.R[n;m];n,m.T[n;m];l;a)\mkleeneclose{}
                ;  \mkleeneopen{}\mlambda{}\msubtwo{}l  a.\mforall{}s:StrictInc
                                      \mexists{}n:\mBbbN{}
                                        (baf-bar(n,m.R[n;m];n,m.T[n;m];l  +  1;a.s  n@l)
                                        \mvee{}  (\mexists{}n:\mBbbN{}.  \mexists{}m:\{n  +  1...\}.  (R[n;m]  \mwedge{}  T[n;m])))\mkleeneclose{}
                ]\mcdot{}
              THENW  Auto
              )
  )

---

Home Index