---

Step * 2 of Lemma mul-distributes


1. ∀x,y,z:ℤ.  ((x * (y + z)) = ((x * y) + (x * z)) ∈ ℤ)
⊢ ∀[x,y,z:Top].  (x * (y + z) ~ (x * y) + (x * z))
BY
{ TACTIC:(SqReasoning
          THEN Try (((InstHyp [⌜x⌝;⌜y⌝;⌜z⌝] 1⋅ THENA Trivial) THEN HypSubst' (-1) 0 THEN Auto))
          THEN Try (OnMaybeHyp 8 (\h. (ExceptionSqequal h⋅
                                       THEN HypSubst' (-1) 0
                                       THEN (Reduce 0
                                             THEN (RWW "int-mul-exception int-add-exception" 0 THENA Auto)
                                             THEN Reduce 0)
                                       THEN Complete (Auto))))) }

1
1. ∀x,y,z:ℤ.  ((x * (y + z)) = ((x * y) + (x * z)) ∈ ℤ)
2. z : Base
3. y : Base
4. x : Base
5. is-exception((x * y) + (x * z))
6. x * y ∈ ℤ
7. is-exception(x * z)
8. (x * y)↓
9. x ∈ ℤ
10. y ∈ ℤ
⊢ (x * y) + (x * z) ≤ x * (y + z)

---

Latex:

---

Latex:

1.  \mforall{}x,y,z:\mBbbZ{}.    ((x  *  (y  +  z))  =  ((x  *  y)  +  (x  *  z)))
\mvdash{}  \mforall{}[x,y,z:Top].    (x  *  (y  +  z)  \msim{}  (x  *  y)  +  (x  *  z))


By

---

Latex:
TACTIC:(SqReasoning
                THEN  Try  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  1\mcdot{}  THENA  Trivial)  THEN  HypSubst'  (-1)  0  THEN  Auto))
                THEN  Try  (OnMaybeHyp  8  (\mbackslash{}h.  (ExceptionSqequal  h\mcdot{}
                                                                          THEN  HypSubst'  (-1)  0
                                                                          THEN  (Reduce  0
                                                                                      THEN  (RWW  "int-mul-exception  int-add-exception"  0
                                                                                                  THENA  Auto
                                                                                                  )
                                                                                      THEN  Reduce  0)
                                                                          THEN  Complete  (Auto)))))

---

Home Index