---

Step * of Lemma partial_ap_compose

∀[g:Top]. ∀[m1:ℕ]. ∀[m2:ℕm1 + 1]. ∀[m3:ℕm2 + 1].  (partial_ap(partial_ap(g;m1;m2);m2;m3) ~ partial_ap(g;m1;m3))
BY
{ ((UnivCD THENA Auto)
   THEN (RW (AddrC [1;1] (LemmaC `partial_ap_is_gen`)) 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `partial_ap_is_gen`)) 0 THENA Auto)
   THEN BLemma `partial_ap_of_partial_ap_gen`
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[g:Top].  \mforall{}[m1:\mBbbN{}].  \mforall{}[m2:\mBbbN{}m1  +  1].  \mforall{}[m3:\mBbbN{}m2  +  1].
    (partial\_ap(partial\_ap(g;m1;m2);m2;m3)  \msim{}  partial\_ap(g;m1;m3))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `partial\_ap\_is\_gen`))  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `partial\_ap\_is\_gen`))  0  THENA  Auto)
  THEN  BLemma  `partial\_ap\_of\_partial\_ap\_gen`
  THEN  Auto')

---

Home Index