Step * 1 of Lemma productdeq_reduce_lemma


1. Top@i
2. Top@i
3. Top@i
4. Top@i
5. Top@i
6. Top@i
7. Top@i
8. Top@i
⊢ product-deq(A;B;a;b) <x, y> <u, v> (a u) ∧b (b v)
BY
Try (RW (AddrC [1] (UnfoldC `product-deq` ANDTHENC ReduceC)) 0)⋅ }

1
1. Top@i
2. Top@i
3. Top@i
4. Top@i
5. Top@i
6. Top@i
7. Top@i
8. Top@i
⊢ (a u) ∧b (b v) (a u) ∧b (b v)


Latex:


Latex:

1.  v  :  Top@i
2.  u  :  Top@i
3.  y  :  Top@i
4.  x  :  Top@i
5.  b  :  Top@i
6.  a  :  Top@i
7.  B  :  Top@i
8.  A  :  Top@i
\mvdash{}  product-deq(A;B;a;b)  <x,  y>  <u,  v>  \msim{}  (a  x  u)  \mwedge{}\msubb{}  (b  y  v)


By


Latex:
Try  (RW  (AddrC  [1]  (UnfoldC  `product-deq`  ANDTHENC  ReduceC))  0)\mcdot{}




Home Index