---

Step * 1 of Lemma assoc_shift


1. A : Type
2. B : Type
3. opa : A ⟶ A ⟶ A
4. opb : B ⟶ B ⟶ B
5. f : A ⟶ B
6. ∀a1,a2:A.  (((f a1) = (f a2) ∈ B) ⇒ (a1 = a2 ∈ A))
7. ∀[a1,a2:A].  ((f (a1 opa a2)) = ((f a1) opb (f a2)) ∈ B)
8. ∀[x,y,z:B].  ((x opb (y opb z)) = ((x opb y) opb z) ∈ B)
9. x : A
10. y : A
11. z : A
⊢ (x opa (y opa z)) = ((x opa y) opa z) ∈ A
BY
{ ((BHyp 6 
THENM RWW "7" 0 
THENM BHyp 8) THENA Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  opa  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
4.  opb  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  f  :  A  {}\mrightarrow{}  B
6.  \mforall{}a1,a2:A.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))
7.  \mforall{}[a1,a2:A].    ((f  (a1  opa  a2))  =  ((f  a1)  opb  (f  a2)))
8.  \mforall{}[x,y,z:B].    ((x  opb  (y  opb  z))  =  ((x  opb  y)  opb  z))
9.  x  :  A
10.  y  :  A
11.  z  :  A
\mvdash{}  (x  opa  (y  opa  z))  =  ((x  opa  y)  opa  z)


By

---

Latex:
((BHyp  6 
THENM  RWW  "7"  0 
THENM  BHyp  8)  THENA  Auto)

---

Home Index