Step * 1 1 of Lemma mul-assoced-one

.....assertion..... 
1. : ℤ@i
2. : ℤ@i
3. (x y) 1@i
4. (x y)@i
⊢ (x y)
BY
(UnfoldTopAb THEN InstConcl [⌜y⌝]⋅ THEN Auto) }


Latex:


Latex:
.....assertion..... 
1.  x  :  \mBbbZ{}@i
2.  y  :  \mBbbZ{}@i
3.  (x  *  y)  |  1@i
4.  1  |  (x  *  y)@i
\mvdash{}  x  |  (x  *  y)


By


Latex:
(UnfoldTopAb  0  THEN  InstConcl  [\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)




Home Index