---

Step * of Lemma es-interface-accum-programmable

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[x:B]. ∀[f:B ⟶ A ⟶ B].
  (es-interface-accum(f;x;X)
  = λB,r. if (#(B 0) =z 1)
         then if (#(r) =z 1) then {f[only(r);only(B 0)]} else {f[x;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 2⋅))
                )
         )⋅
   THEN (RenameVar `Y' (-2)
         THEN Assert ⌜∀es:EO+(Info). ∀e:E.
                        ((Y es e)
                        = if (#(X es e) =z 1)
                          then if (#(Prior(Y) es e) =z 1)
                               then {f[only(Prior(Y) es e);only(X es e)]}
                               else {f[x;only(X es e)]}
                               fi 
                          else {}
                          fi 
                        ∈ bag(B))⌝⋅
         )⋅) }

1
.....assertion..... 
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. x : B
6. f : B ⟶ A ⟶ B
7. Y : EClass(B)@i'
8. λB,r. if (#(B 0) =z 1)
        then if (#(r) =z 1) then {f[only(r);only(B 0)]} else {f[x;only(B 0)]} fi 
        else {}
        fi |λi.X,(self)'|
= Y
∈ EClass(B)@i'
⊢ ∀es:EO+(Info). ∀e:E.
    ((Y es e)
    = if (#(X es e) =z 1)
      then if (#(Prior(Y) es e) =z 1) then {f[only(Prior(Y) es e);only(X es e)]} else {f[x;only(X es e)]} fi 
      else {}
      fi 
    ∈ bag(B))

2
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. x : B
6. f : B ⟶ A ⟶ B
7. Y : EClass(B)@i'
8. λB,r. if (#(B 0) =z 1)
        then if (#(r) =z 1) then {f[only(r);only(B 0)]} else {f[x;only(B 0)]} fi 
        else {}
        fi |λi.X,(self)'|
= Y
∈ EClass(B)@i'
9. ∀es:EO+(Info). ∀e:E.
     ((Y es e)
     = if (#(X es e) =z 1)
       then if (#(Prior(Y) es e) =z 1) then {f[only(Prior(Y) es e);only(X es e)]} else {f[x;only(X es e)]} fi 
       else {}
       fi 
     ∈ bag(B))
⊢ es-interface-accum(f;x;X) = Y ∈ EClass(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[x:B].  \mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].
    (es-interface-accum(f;x;X)
    =  \mlambda{}B,r.  if  (\#(B  0)  =\msubz{}  1)
                  then  if  (\#(r)  =\msubz{}  1)  then  \{f[only(r);only(B  0)]\}  else  \{f[x;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  2\mcdot{}))
                            )
              )\mcdot{}
  THEN  (RenameVar  `Y'  (-2)
              THEN  Assert  \mkleeneopen{}\mforall{}es:EO+(Info).  \mforall{}e:E.
                                            ((Y  es  e)
                                            =  if  (\#(X  es  e)  =\msubz{}  1)
                                                then  if  (\#(Prior(Y)  es  e)  =\msubz{}  1)
                                                          then  \{f[only(Prior(Y)  es  e);only(X  es  e)]\}
                                                          else  \{f[x;only(X  es  e)]\}
                                                          fi 
                                                else  \{\}
                                                fi  )\mkleeneclose{}\mcdot{}
              )\mcdot{})

---

Home Index