---

Step * of Lemma no_repeats-length-equal-by-relation

No Annotations
∀[A,B:Type]. ∀[as:A List]. ∀[bs:B List].
  (||as|| = ||bs|| ∈ ℤ) supposing 
     ((∃R:A ⟶ B ⟶ ℙ
        ((∀a1,a2:A. ∀b:B.  ((a1 ∈ as) ⇒ (a2 ∈ as) ⇒ (b ∈ bs) ⇒ (R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
        ∧ (∀b1,b2:B. ∀a:A.  ((b1 ∈ bs) ⇒ (b2 ∈ bs) ⇒ (a ∈ as) ⇒ (R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
        ∧ (∀a∈as.(∃b∈bs. R a b))
        ∧ (∀b∈bs.(∃a∈as. R a b)))) and 
     no_repeats(A;as) and 
     no_repeats(B;bs))
BY
{ ((Assert ∀[A,B:Type]. ∀[as:A List]. ∀[bs:B List].
             (||as|| = ||bs|| ∈ ℤ) supposing 
                ((∃R:A ⟶ B ⟶ ℙ
                   ((∀a1,a2:A. ∀b:B.  ((R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
                   ∧ (∀b1,b2:B. ∀a:A.  ((R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
                   ∧ (∀a∈as.(∃b∈bs. R a b))
                   ∧ (∀b∈bs.(∃a∈as. R a b)))) and 
                no_repeats(A;as) and 
                no_repeats(B;bs)) BY
          (Auto
           THEN ExRepD
           THEN (InstLemma `no_repeats-length-le-by-relation` [⌜A⌝;⌜B⌝;⌜R⌝;⌜as⌝;⌜bs⌝]⋅ THENA Auto)
           THEN InstLemma `no_repeats-length-le-by-relation` [⌜B⌝;⌜A⌝;⌜λb,a. (R a b)⌝;⌜bs⌝;⌜as⌝]⋅
           THEN Auto
           THEN All Reduce
           THEN Auto))
   THEN RepeatFor 7 (ParallelLast')
   ) }

1
.....antecedent..... 
1. A : Type
2. B : Type
3. as : A List
4. bs : B List
5. no_repeats(B;bs)
6. no_repeats(A;as)
7. ∃R:A ⟶ B ⟶ ℙ
    ((∀a1,a2:A. ∀b:B.  ((a1 ∈ as) ⇒ (a2 ∈ as) ⇒ (b ∈ bs) ⇒ (R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
    ∧ (∀b1,b2:B. ∀a:A.  ((b1 ∈ bs) ⇒ (b2 ∈ bs) ⇒ (a ∈ as) ⇒ (R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
    ∧ (∀a∈as.(∃b∈bs. R a b))
    ∧ (∀b∈bs.(∃a∈as. R a b)))
⊢ ∃R:A ⟶ B ⟶ ℙ
   ((∀a1,a2:A. ∀b:B.  ((R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
   ∧ (∀b1,b2:B. ∀a:A.  ((R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
   ∧ (∀a∈as.(∃b∈bs. R a b))
   ∧ (∀b∈bs.(∃a∈as. R a b)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:Type].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].
    (||as||  =  ||bs||)  supposing 
          ((\mexists{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
                ((\mforall{}a1,a2:A.  \mforall{}b:B.
                        ((a1  \mmember{}  as)  {}\mRightarrow{}  (a2  \mmember{}  as)  {}\mRightarrow{}  (b  \mmember{}  bs)  {}\mRightarrow{}  (R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2)))
                \mwedge{}  (\mforall{}b1,b2:B.  \mforall{}a:A.
                          ((b1  \mmember{}  bs)  {}\mRightarrow{}  (b2  \mmember{}  bs)  {}\mRightarrow{}  (a  \mmember{}  as)  {}\mRightarrow{}  (R  a  b1)  {}\mRightarrow{}  (R  a  b2)  {}\mRightarrow{}  (b1  =  b2)))
                \mwedge{}  (\mforall{}a\mmember{}as.(\mexists{}b\mmember{}bs.  R  a  b))
                \mwedge{}  (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  R  a  b))))  and 
          no\_repeats(A;as)  and 
          no\_repeats(B;bs))


By

---

Latex:
((Assert  \mforall{}[A,B:Type].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].
                      (||as||  =  ||bs||)  supposing 
                            ((\mexists{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
                                  ((\mforall{}a1,a2:A.  \mforall{}b:B.    ((R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2)))
                                  \mwedge{}  (\mforall{}b1,b2:B.  \mforall{}a:A.    ((R  a  b1)  {}\mRightarrow{}  (R  a  b2)  {}\mRightarrow{}  (b1  =  b2)))
                                  \mwedge{}  (\mforall{}a\mmember{}as.(\mexists{}b\mmember{}bs.  R  a  b))
                                  \mwedge{}  (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  R  a  b))))  and 
                            no\_repeats(A;as)  and 
                            no\_repeats(B;bs))  BY
                (Auto
                  THEN  ExRepD
                  THEN  (InstLemma  `no\_repeats-length-le-by-relation`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  InstLemma  `no\_repeats-length-le-by-relation`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}b,a.  (R  a  b)\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}
                  THEN  Auto
                  THEN  All  Reduce
                  THEN  Auto))
  THEN  RepeatFor  7  (ParallelLast')
  )

---

Home Index