---

Step * of Lemma agree_on_common_cons2

∀[T:Type]
  ∀as,bs:T List. ∀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
{ (Intro
   THEN (Assert ∀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))))
        THENM ((RepeatFor 2 (D 0 THENA Auto) THEN InstHyp [||as|| + ||bs||;as;bs] 2) THEN Auto)
        )
   ) }

1
.....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))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}as,bs:T  List.  \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:
(Intro
  THEN  (Assert  \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))))
            THENM  ((RepeatFor  2  (D  0  THENA  Auto)  THEN  InstHyp  [||as||  +  ||bs||;as;bs]  2)  THEN  Auto)
            )
  )

---

Home Index