---

Step * 2 2 1 2 of Lemma polymorphic-choice-int


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. ¬((f 0 1) = 0 ∈ ℤ)
5. x : ℤ
6. y : ℤ
7. (f 0 1) = 1 ∈ Base
8. (f x y) = x ∈ Base
9. ¬(x = y ∈ ℤ)
10. (f 2 3) = 3 ∈ Base
⊢ ∃n,m:ℤ. ((¬(n = m ∈ ℤ)) ∧ ((f n m) = m ∈ ℤ) ∧ (¬(x = m ∈ ℤ)) ∧ (¬(y = n ∈ ℤ)))
BY
{ (Assert (f 4 5) = 5 ∈ Base BY
         ((InstHyp [⌜4⌝;⌜5⌝] 2⋅ THENA Auto) THEN RepeatFor 2 (D -1) THEN Auto)) }

1
.....aux..... 
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. ¬((f 0 1) = 0 ∈ ℤ)
5. x : ℤ
6. y : ℤ
7. (f 0 1) = 1 ∈ Base
8. (f x y) = x ∈ Base
9. ¬(x = y ∈ ℤ)
10. (f 2 3) = 3 ∈ Base
11. (f 4 5) = 4 ∈ Base
⊢ (f 4 5) = 5 ∈ Base

2
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. f ∈ ℤ ⟶ ℤ ⟶ ℤ
4. ¬((f 0 1) = 0 ∈ ℤ)
5. x : ℤ
6. y : ℤ
7. (f 0 1) = 1 ∈ Base
8. (f x y) = x ∈ Base
9. ¬(x = y ∈ ℤ)
10. (f 2 3) = 3 ∈ Base
11. (f 4 5) = 5 ∈ Base
⊢ ∃n,m:ℤ. ((¬(n = m ∈ ℤ)) ∧ ((f n m) = m ∈ ℤ) ∧ (¬(x = m ∈ ℤ)) ∧ (¬(y = n ∈ ℤ)))

---

Latex:

---

Latex:

1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
2.  \mforall{}x,y:Base.    (\mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y))
3.  f  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
4.  \mneg{}((f  0  1)  =  0)
5.  x  :  \mBbbZ{}
6.  y  :  \mBbbZ{}
7.  (f  0  1)  =  1
8.  (f  x  y)  =  x
9.  \mneg{}(x  =  y)
10.  (f  2  3)  =  3
\mvdash{}  \mexists{}n,m:\mBbbZ{}.  ((\mneg{}(n  =  m))  \mwedge{}  ((f  n  m)  =  m)  \mwedge{}  (\mneg{}(x  =  m))  \mwedge{}  (\mneg{}(y  =  n)))


By

---

Latex:
(Assert  (f  4  5)  =  5  BY
              ((InstHyp  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}5\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  Auto))

---

Home Index