---

Step * of Lemma accum-class-programmable

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[base:A ─→ B]. ∀[f:B ─→ A ─→ B].
  (accum-class(b,a.f[b;a];a.base[a];X)
  = λB,r. if (#(B 0) =z 1)
         then if (#(r) =z 1) then {f[only(r);only(B 0)]} else {base[only(B 0)]} fi 
         else {}
         fi |λi.X,(self)'|
  ∈ EClass(B))
BY
{ (Auto
   THEN (GenConclAtAddrType ⌈EClass(B)⌉ [3]⋅
         THENA (Try (Complete (Auto))
                THEN Try (((InstLemma `rec-combined-class_wf` [⌈Info⌉;⌈1⌉;⌈λ2n.A⌉]⋅ THENA Auto)
                           THEN BHyp (-1)
                           THEN Auto
                           THEN EAuto 1⋅))
                )
         )
   ) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. base : A ─→ B
6. f : B ─→ A ─→ B
7. v : EClass(B)@i'
8. λB,r. if (#(B 0) =z 1)
        then if (#(r) =z 1) then {f[only(r);only(B 0)]} else {base[only(B 0)]} fi 
        else {}
        fi |λi.X,(self)'|
= v
∈ EClass(B)@i'
⊢ accum-class(b,a.f[b;a];a.base[a];X) = v ∈ EClass(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[base:A  {}\mrightarrow{}  B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (accum-class(b,a.f[b;a];a.base[a];X)
    =  \mlambda{}B,r.  if  (\#(B  0)  =\msubz{}  1)
                  then  if  (\#(r)  =\msubz{}  1)  then  \{f[only(r);only(B  0)]\}  else  \{base[only(B  0)]\}  fi 
                  else  \{\}
                  fi  |\mlambda{}i.X,(self)'|)


By

---

Latex:
(Auto
  THEN  (GenConclAtAddrType  \mkleeneopen{}EClass(B)\mkleeneclose{}  [3]\mcdot{}
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  (((InstLemma  `rec-combined-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.A\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                  THEN  BHyp  (-1)
                                                  THEN  Auto
                                                  THEN  EAuto  1\mcdot{}))
                            )
              )
  )

---

Home Index