---

Step * of Lemma K_uforces_quant_lemma

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

---

Latex:

---

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


By

---

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

---

Home Index