---

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

.....assertion..... 
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) = 2 ∈ Base
⊢ 1 = 2 ∈ ℤ_2
BY
{ (((Assert (f 0 1) = 1 ∈ ℤ_2 BY (HypSubst' 7 0 THEN Auto)) THEN MoveToConcl (-1))
   THEN ((Assert (f 2 3) = 2 ∈ ℤ_2 BY (HypSubst' (-1) 0 THEN Auto)) THEN MoveToConcl (-1))
   THEN (GenConcl ⌜f = g ∈ (ℤ_2 ⟶ ℤ_2 ⟶ ℤ_2)⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. g : ℤ_2 ⟶ ℤ_2 ⟶ ℤ_2
2. (g 2 3) = 2 ∈ ℤ_2
3. (g 0 1) = 1 ∈ ℤ_2
⊢ 1 = 2 ∈ ℤ_2

---

Latex:

---

Latex:
.....assertion..... 
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)  =  2
\mvdash{}  1  =  2


By

---

Latex:
(((Assert  (f  0  1)  =  1  BY  (HypSubst'  7  0  THEN  Auto))  THEN  MoveToConcl  (-1))
  THEN  ((Assert  (f  2  3)  =  2  BY  (HypSubst'  (-1)  0  THEN  Auto))  THEN  MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index