---

Step * 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))
⊢ (∀x,y:ℤ.  ((f x y) = x ∈ ℤ)) ∨ (∀x,y:ℤ.  ((f x y) = y ∈ ℤ))
BY
{ ((Assert f ∈ ℤ ⟶ ℤ ⟶ ℤ BY
          Auto)
   THEN ((Decide (f 0 1) = 0 ∈ ℤ THENA Auto)
         THENL [(OrLeft THEN Auto)
               ; (OrRight
                  THEN Auto
                  THEN (InstHyp [⌜0⌝;⌜1⌝] 2⋅ THENA Auto)
                  THEN RepeatFor 2 (D -1)
                  THEN Try ((DNot 4 THEN HypSubst' (-1) 0 THEN Fold `member` 0 THEN Auto)))]
   )
   THEN (InstHyp [⌜x⌝;⌜y⌝] 2⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN Try ((HypSubst' (-1) 0 THEN Complete (Auto)))
   THEN Decide x = y ∈ ℤ
   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 x y) = y ∈ Base
8. ¬(x = y ∈ ℤ)
⊢ (f x y) = x ∈ ℤ

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 ∈ ℤ)
⊢ (f x y) = y ∈ ℤ

---

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))
\mvdash{}  (\mforall{}x,y:\mBbbZ{}.    ((f  x  y)  =  x))  \mvee{}  (\mforall{}x,y:\mBbbZ{}.    ((f  x  y)  =  y))


By

---

Latex:
((Assert  f  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  BY
                Auto)
  THEN  ((Decide  (f  0  1)  =  0  THENA  Auto)
              THENL  [(OrLeft  THEN  Auto)
                          ;  (OrRight
                                THEN  Auto
                                THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
                                THEN  RepeatFor  2  (D  -1)
                                THEN  Try  ((DNot  4  THEN  HypSubst'  (-1)  0  THEN  Fold  `member`  0  THEN  Auto)))]
  )
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Try  ((HypSubst'  (-1)  0  THEN  Complete  (Auto)))
  THEN  Decide  x  =  y
  THEN  Auto)

---

Home Index