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

.....aux..... 
1. : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f y) x ∈ Base) ∨ ((f y) y ∈ Base))
3. ∀z:Base. ((f z) z ∈ Base)
4. ((f 1) 0 ∈ Base) ∨ ((f 1) 1 ∈ Base)
5. 0 ∈ Base
6. ∀x,y:ℤ.  ((f y) x ∈ ℤ)
7. (f 0) 1 ∈ ℤ
8. ∀y:Base. ((f y) 1 ∈ Base)
9. Base
⊢ (f 0) x ∈ Base
BY
((Assert ↓((f 0) x ∈ Base) ∨ ((f 0) 0 ∈ Base) BY
          Auto)
   THEN RepeatFor (D -1)
   THEN Try (Trivial)
   THEN (InstLemma `type-with-y=n` [⌜1⌝;⌜0⌝;⌜x⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert f ∈ T ⟶ T ⟶ BY
               Auto)
   THEN (Assert (f 0) (f 0) ∈ BY
               RepeatFor ((EqCD THEN Try (Eq))))) }

1
1. : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f y) x ∈ Base) ∨ ((f y) y ∈ Base))
3. ∀z:Base. ((f z) z ∈ Base)
4. ((f 1) 0 ∈ Base) ∨ ((f 1) 1 ∈ Base)
5. 0 ∈ Base
6. ∀x,y:ℤ.  ((f y) x ∈ ℤ)
7. (f 0) 1 ∈ ℤ
8. ∀y:Base. ((f y) 1 ∈ Base)
9. Base
10. (f 0) 0 ∈ Base
11. Type
12. 1 ∈ T
13. 0 ∈ T
14. (1 0 ∈ T)  (x 0 ∈ Base)
15. f ∈ T ⟶ T ⟶ T
16. (f 0) (f 0) ∈ T
⊢ (f 0) x ∈ Base


Latex:


Latex:
.....aux..... 
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.  \mforall{}z:Base.  ((f  z  z)  =  z)
4.  ((f  0  1)  =  0)  \mvee{}  ((f  0  1)  =  1)
5.  0  =  0
6.  \mforall{}x,y:\mBbbZ{}.    ((f  x  y)  =  x)
7.  (f  1  0)  =  1
8.  \mforall{}y:Base.  ((f  1  y)  =  1)
9.  x  :  Base
\mvdash{}  (f  x  0)  =  x


By


Latex:
((Assert  \mdownarrow{}((f  x  0)  =  x)  \mvee{}  ((f  x  0)  =  0)  BY
                Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Try  (Trivial)
  THEN  (InstLemma  `type-with-y=n`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  f  \mmember{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T  BY
                          Auto)
  THEN  (Assert  (f  1  0)  =  (f  x  0)  BY
                          RepeatFor  2  ((EqCD  THEN  Try  (Eq)))))




Home Index