---

Step * 2 of Lemma deq-f-subset_wf


1. T : Type
2. eq : EqDecider(T)
⊢ λx,y. isl(TERMOF{decidable__f-subset:o, \\v:l, i:l} eq x y) ∈ {d:fset(T) ⟶ fset(T) ⟶ 𝔹| 
                                                             ∀x,y:fset(T).  (x ⊆ y ⇐⇒ ↑(d x y))} 
BY
{ (MemTypeCD
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (((MemCD THENA Auto) ORELSE (D 0 THENA Auto)))
   THEN GenConcl ⌜(TERMOF{decidable__f-subset:o, \\v:l, i:l} eq x y) = d ∈ Dec(x ⊆ y)⌝⋅
   THEN Auto
   THEN Try ((GenConclAtAddrType ⌜∀xs,ys:fset(T).  Dec(xs ⊆ ys)⌝ [2;1;1]⋅ THEN Auto))
   THEN DVar `d'
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mlambda{}x,y.  isl(TERMOF\{decidable\_\_f-subset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  eq  x  y)  \mmember{}  \{d:fset(T)  {}\mrightarrow{}  fset(T)  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                          \mforall{}x,y:fset(T).    (x  \msubseteq{}  y  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  x  y))\} 


By

---

Latex:
(MemTypeCD
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (((MemCD  THENA  Auto)  ORELSE  (D  0  THENA  Auto)))
  THEN  GenConcl  \mkleeneopen{}(TERMOF\{decidable\_\_f-subset:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  eq  x  y)  =  d\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  ((GenConclAtAddrType  \mkleeneopen{}\mforall{}xs,ys:fset(T).    Dec(xs  \msubseteq{}  ys)\mkleeneclose{}  [2;1;1]\mcdot{}  THEN  Auto))
  THEN  DVar  `d'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index