---

Step * of Lemma K_forces_quant_lemma

∀body,z,isall,K:Top.
  (K-forces(K;mFOquant(isall;z;body)) ~ if isall
  then λi,a. ∀j:{j:World| i ≤ j} . ∀v:Dom(j).  (K-forces(K;body) j a[z := v])
  else λi,a. ∃v:Dom(i). (K-forces(K;body) i a[z := v])
  fi )
BY
{ ((UnivCD THENA Auto) THEN Unfold `K-forces` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}body,z,isall,K:Top.
    (K-forces(K;mFOquant(isall;z;body))  \msim{}  if  isall
    then  \mlambda{}i,a.  \mforall{}j:\{j:World|  i  \mleq{}  j\}  .  \mforall{}v:Dom(j).    (K-forces(K;body)  j  a[z  :=  v])
    else  \mlambda{}i,a.  \mexists{}v:Dom(i).  (K-forces(K;body)  i  a[z  :=  v])
    fi  )


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `K-forces`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index