---

Step * of Lemma flip_twice

∀[k:ℤ]. ∀[x,y,i:ℕk].  (((y, x) ((y, x) i)) = i ∈ ℤ)
BY
{ (Auto THEN Subst (y, x) ((y, x) i) ~ ((y, x) o (y, x)) i 0) }

1
.....equality..... 
1. k : ℤ
2. x : ℕk
3. y : ℕk
4. i : ℕk
⊢ (y, x) ((y, x) i) ~ ((y, x) o (y, x)) i

2
1. k : ℤ
2. x : ℕk
3. y : ℕk
4. i : ℕk
⊢ (((y, x) o (y, x)) i) = i ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[x,y,i:\mBbbN{}k].    (((y,  x)  ((y,  x)  i))  =  i)


By

---

Latex:
(Auto  THEN  Subst  (y,  x)  ((y,  x)  i)  \msim{}  ((y,  x)  o  (y,  x))  i  0)

---

Home Index