---

Step * 1 2 1 1 of Lemma agree_on_common_cons2


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))))
5. as : T List
6. x : T
7. u : T
8. v : T List
9. ((||as|| + ||v||) ≤ n) ⇒ agree_on_common(T;[x / as];v) ⇐⇒ agree_on_common(T;as;v) supposing ¬(x ∈ v)
10. (||as|| + ||[u / v]||) ≤ n
11. ¬(x ∈ [u / v])
12. agree_on_common(T;[x / as];[u / v])
⊢ agree_on_common(T;as;[u / v])
BY
{ ((((RecUnfold `agree_on_common` (-1) THEN Reduce (-1)) THEN SimpHyp (-1)) THEN D (-1)) THEN Auto) }

1
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))))
5. as : T List
6. x : T
7. u : T
8. v : T List
9. ((||as|| + ||v||) ≤ n) ⇒ agree_on_common(T;[x / as];v) ⇐⇒ agree_on_common(T;as;v) supposing ¬(x ∈ v)
10. (||as|| + ||[u / v]||) ≤ n
11. ¬(x ∈ [u / v])
12. ((¬(u ∈ [x / as])) ∧ agree_on_common(T;[x / as];v)) ∨ ((x = u ∈ T) ∧ agree_on_common(T;as;v))
⊢ agree_on_common(T;as;[u / v])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  n
4.  \mforall{}as,bs:T  List.
          (((||as||  +  ||bs||)  \mleq{}  (n  -  1))
          {}\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))))
5.  as  :  T  List
6.  x  :  T
7.  u  :  T
8.  v  :  T  List
9.  ((||as||  +  ||v||)  \mleq{}  n)
{}\mRightarrow{}  agree\_on\_common(T;[x  /  as];v)  \mLeftarrow{}{}\mRightarrow{}  agree\_on\_common(T;as;v)  supposing  \mneg{}(x  \mmember{}  v)
10.  (||as||  +  ||[u  /  v]||)  \mleq{}  n
11.  \mneg{}(x  \mmember{}  [u  /  v])
12.  agree\_on\_common(T;[x  /  as];[u  /  v])
\mvdash{}  agree\_on\_common(T;as;[u  /  v])


By

---

Latex:
((((RecUnfold  `agree\_on\_common`  (-1)  THEN  Reduce  (-1))  THEN  SimpHyp  (-1))  THEN  D  (-1))  THEN  Auto)

---

Home Index