---

Step * of Lemma FOL-hyps-meaning-cons

∀[hyps,Dom,S,a,x:Top].
  (tuple-type(FOL-hyps-meaning(Dom;S;a;[x / hyps])) ~ if null(hyps)
  then Dom,S,a +|= FOL-abstract(x)
  else Dom,S,a +|= FOL-abstract(x) × tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
  fi )
BY
{ ((Auto THEN RepUR ``FOL-hyps-meaning`` 0) THEN RWO "null-map" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[hyps,Dom,S,a,x:Top].
    (tuple-type(FOL-hyps-meaning(Dom;S;a;[x  /  hyps]))  \msim{}  if  null(hyps)
    then  Dom,S,a  +|=  FOL-abstract(x)
    else  Dom,S,a  +|=  FOL-abstract(x)  \mtimes{}  tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
    fi  )


By

---

Latex:
((Auto  THEN  RepUR  ``FOL-hyps-meaning``  0)  THEN  RWO  "null-map"  0  THEN  Auto)

---

Home Index