---

Step * 2 2 2 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. n : ℤ
11. m : ℤ
12. ¬(n = m ∈ ℤ)
13. (f n m) = m ∈ ℤ
14. ¬(x = m ∈ ℤ)
15. ¬(y = n ∈ ℤ)
16. ∃T:Type. ((x = n ∈ T) ∧ (y = m ∈ T) ∧ (¬(x = y ∈ T)))
⊢ (f x y) = y ∈ ℤ
BY
{ (ExRepD
   THEN (Assert (f x y) = x ∈ T BY
               (HypSubst' 8 0 THEN Eq))
   THEN (Assert (f n m) = m ∈ T BY
               (HypSubst' 13 0 THEN Eq))
   THEN (Assert ⌜False⌝⋅ THENM Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜f = g ∈ (T ⟶ T ⟶ T)⌝⋅ THENA (All Thin THEN Auto))) }

1
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. n : ℤ
11. m : ℤ
12. ¬(n = m ∈ ℤ)
13. (f n m) = m ∈ ℤ
14. ¬(x = m ∈ ℤ)
15. ¬(y = n ∈ ℤ)
16. T : Type
17. x = n ∈ T
18. y = m ∈ T
19. ¬(x = y ∈ T)
20. g : T ⟶ T ⟶ T
21. f = g ∈ (T ⟶ T ⟶ T)
⊢ ((g x y) = x ∈ T) ⇒ ((g n m) = m ∈ T) ⇒ False

---

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.  n  :  \mBbbZ{}
11.  m  :  \mBbbZ{}
12.  \mneg{}(n  =  m)
13.  (f  n  m)  =  m
14.  \mneg{}(x  =  m)
15.  \mneg{}(y  =  n)
16.  \mexists{}T:Type.  ((x  =  n)  \mwedge{}  (y  =  m)  \mwedge{}  (\mneg{}(x  =  y)))
\mvdash{}  (f  x  y)  =  y


By

---

Latex:
(ExRepD
  THEN  (Assert  (f  x  y)  =  x  BY
                          (HypSubst'  8  0  THEN  Eq))
  THEN  (Assert  (f  n  m)  =  m  BY
                          (HypSubst'  13  0  THEN  Eq))
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  (All  Thin  THEN  Auto)))

---

Home Index