---

Step * of Lemma simple-loc-comb-2-concat-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B,C:Type]. ∀[F:Id ─→ A ─→ B ─→ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  single-valued-classrel(es;F@Loc o (Loc,X, Y);C) 
  supposing (∀i:Id. ∀a:A. ∀b:B.  (#(F i a b) ≤ 1)) ∧ single-valued-classrel(es;X;A) ∧ single-valued-classrel(es;Y;B)
BY
{ (Unfold `single-valued-classrel` 0
   THEN (UnivCD THENA MaAuto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN (InstHyp [⌈e⌉;⌈a⌉;⌈a1⌉] (-15)⋅ THENA Auto)
   THEN (InstHyp [⌈e⌉;⌈b⌉;⌈b1⌉] (-15)⋅ THENA Auto)
   THEN (InstHyp [⌈loc(e)⌉;⌈a⌉;⌈b⌉] (-18)⋅ THENA Auto)
   THEN (Assert ⌈(#(F loc(e) a b) ≤ 0) ∨ (#(F loc(e) a b) = 1 ∈ ℤ)⌉⋅ THENA MaAuto)
   THEN D (-1)
   THEN Try (Complete (((FLemma `bag-size-zero` [-1] THENA Auto)
                        THEN (RWO "-1" (-11) THENA Auto)
                        THEN BagMemberD (-11))))
   THEN (Eliminate ⌈a1⌉⋅ THENA Auto)
   THEN (Eliminate ⌈b1⌉⋅ THENA Auto)
   THEN ThinVar `a1'
   THEN ThinVar `b1'
   THEN (FLemma `bag-size-one` [-1] THENA Auto)
   THEN MoveToConcl (-4)
   THEN MoveToConcl (-6)
   THEN HypSubst' (-1) 0
   THEN (GenConclAtAddr [1;3;1] THENA Auto)
   THEN Try ((All Thin THEN Auto THEN BagMemberD (-2) THEN BagMemberD (-1) THEN Auto))
   THEN BLemma `single-valued-bag-if-le1`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B,C:Type].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[X:EClass(A)].
\mforall{}[Y:EClass(B)].
    single-valued-classrel(es;F@Loc  o  (Loc,X,  Y);C) 
    supposing  (\mforall{}i:Id.  \mforall{}a:A.  \mforall{}b:B.    (\#(F  i  a  b)  \mleq{}  1))
    \mwedge{}  single-valued-classrel(es;X;A)
    \mwedge{}  single-valued-classrel(es;Y;B)


By

---

Latex:
(Unfold  `single-valued-classrel`  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]  (-15)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  (-15)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-18)\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\#(F  loc(e)  a  b)  \mleq{}  0)  \mvee{}  (\#(F  loc(e)  a  b)  =  1)\mkleeneclose{}\mcdot{}  THENA  MaAuto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((FLemma  `bag-size-zero`  [-1]  THENA  Auto)
                                            THEN  (RWO  "-1"  (-11)  THENA  Auto)
                                            THEN  BagMemberD  (-11))))
  THEN  (Eliminate  \mkleeneopen{}a1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Eliminate  \mkleeneopen{}b1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a1'
  THEN  ThinVar  `b1'
  THEN  (FLemma  `bag-size-one`  [-1]  THENA  Auto)
  THEN  MoveToConcl  (-4)
  THEN  MoveToConcl  (-6)
  THEN  HypSubst'  (-1)  0
  THEN  (GenConclAtAddr  [1;3;1]  THENA  Auto)
  THEN  Try  ((All  Thin  THEN  Auto  THEN  BagMemberD  (-2)  THEN  BagMemberD  (-1)  THEN  Auto))
  THEN  BLemma  `single-valued-bag-if-le1`
  THEN  Auto)

---

Home Index