Step
*
1
1
of Lemma
nonzero-cross-imp_wf
.....equality.....
1. r : IntegDom{i}
2. eq : ∀x,y:|r|. Dec(x = y ∈ |r|)
3. a : {a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))}
4. b : {b:ℕ3 ⟶ |r|| (¬(b = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))}
⊢ nonzero-cross-imp(r;eq;a;b) ~ TERMOF{cross-product-non-zero-implies-ext:o, \\v:l, i:l} r eq a b
BY
{ ((RW (AddrC [2] (TagC (mk_tag_term 1))) 0 THEN Reduce 0) THEN Auto) }
Latex:
Latex:
.....equality.....
1. r : IntegDom\{i\}
2. eq : \mforall{}x,y:|r|. Dec(x = y)
3. a : \{a:\mBbbN{}3 {}\mrightarrow{} |r|| \mneg{}(a = 0)\}
4. b : \{b:\mBbbN{}3 {}\mrightarrow{} |r|| (\mneg{}(b = 0)) \mwedge{} (\mneg{}((a x b) = 0))\}
\mvdash{} nonzero-cross-imp(r;eq;a;b) \msim{} TERMOF\{cross-product-non-zero-implies-ext:o, \mbackslash{}\mbackslash{}v:l, i:l\} r eq a b
By
Latex:
((RW (AddrC [2] (TagC (mk\_tag\_term 1))) 0 THEN Reduce 0) THEN Auto)
Home
Index