Step * of Lemma bpa-equiv_transitivity

p:{2...}. ∀a,b,c:basic-padic(p).  (bpa-equiv(p;a;b)  bpa-equiv(p;b;c)  bpa-equiv(p;a;c))
BY
((D THENA Auto)
   THEN (InstLemma `bpa-equiv-equiv` [⌜p⌝]⋅ THENA Auto)
   THEN RepeatFor (D -1)
   THEN UnfoldTopAb (-1)
   THEN Trivial) }


Latex:


Latex:
\mforall{}p:\{2...\}.  \mforall{}a,b,c:basic-padic(p).    (bpa-equiv(p;a;b)  {}\mRightarrow{}  bpa-equiv(p;b;c)  {}\mRightarrow{}  bpa-equiv(p;a;c))


By


Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `bpa-equiv-equiv`  [\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  UnfoldTopAb  (-1)
  THEN  Trivial)




Home Index