---

Step * of Lemma sequence-class_wf

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)].  (sequence-class(X;Y;Z) ∈ EClass(A))
BY
{ (Auto
   THEN UnfoldAtAddr [2] 0
   THEN UnfoldAtAddr [1] 0
   THEN RepeatFor 2 ((MemCD THENA Auto))
   THEN GenConclAtAddr [2;1]
   THEN Repeat (DProdsAndUnions)
   THEN AllReduce
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(A)].
    (sequence-class(X;Y;Z)  \mmember{}  EClass(A))


By

---

Latex:
(Auto
  THEN  UnfoldAtAddr  [2]  0
  THEN  UnfoldAtAddr  [1]  0
  THEN  RepeatFor  2  ((MemCD  THENA  Auto))
  THEN  GenConclAtAddr  [2;1]
  THEN  Repeat  (DProdsAndUnions)
  THEN  AllReduce
  THEN  Try  (Complete  (Auto)))

---

Home Index