---

Step * 1 of Lemma agree_on_common_cons2

.....assertion..... 
1. [T] : Type
⊢ ∀n:ℕ. ∀as,bs:T List.
    (((||as|| + ||bs||) ≤ n)
    ⇒ (∀x:T
          (agree_on_common(T;[x / as];bs) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ bs)
          ∧ agree_on_common(T;as;[x / bs]) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ as))))
BY
{ InductionOnNat }

1
.....basecase..... 
1. [T] : Type
⊢ ∀as,bs:T List.
    (((||as|| + ||bs||) ≤ 0)
    ⇒ (∀x:T
          (agree_on_common(T;[x / as];bs) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ bs)
          ∧ agree_on_common(T;as;[x / bs]) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ as))))

2
.....upcase..... 
1. [T] : Type
2. n : ℤ
3. [%1] : 0 < n
4. ∀as,bs:T List.
     (((||as|| + ||bs||) ≤ (n - 1))
     ⇒ (∀x:T
           (agree_on_common(T;[x / as];bs) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ bs)
           ∧ agree_on_common(T;as;[x / bs]) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ as))))
⊢ ∀as,bs:T List.
    (((||as|| + ||bs||) ≤ n)
    ⇒ (∀x:T
          (agree_on_common(T;[x / as];bs) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ bs)
          ∧ agree_on_common(T;as;[x / bs]) ⇐⇒ agree_on_common(T;as;bs) supposing ¬(x ∈ as))))

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}as,bs:T  List.
        (((||as||  +  ||bs||)  \mleq{}  n)
        {}\mRightarrow{}  (\mforall{}x:T
                    (agree\_on\_common(T;[x  /  as];bs)  \mLeftarrow{}{}\mRightarrow{}  agree\_on\_common(T;as;bs)  supposing  \mneg{}(x  \mmember{}  bs)
                    \mwedge{}  agree\_on\_common(T;as;[x  /  bs])  \mLeftarrow{}{}\mRightarrow{}  agree\_on\_common(T;as;bs)  supposing  \mneg{}(x  \mmember{}  as))))


By

---

Latex:
InductionOnNat

---

Home Index