---

Step * of Lemma FOL-sequent-evidence-false-hyp

∀hyps:mFOL() List. ∀concl:mFOL(). ∀i:ℕ||hyps||.
  ((↑mFOatomic?(hyps[i]))
  ⇒ (mFOatomic-name(hyps[i]) = "false" ∈ Atom)
  ⇒ (mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List))
  ⇒ FOL-sequent-evidence{i:l}(<hyps, concl>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``FOL-sequent-abstract FOSatWith+`` 0
   THEN Fold `FOSatWith+` 0
   THEN UseWitness ⌜λx.x.i⌝⋅
   THEN Auto
   THEN SubsumeC  ⌜S "false" []⌝⋅
   THEN Auto) }

1
1. hyps : mFOL() List
2. concl : mFOL()
3. i : ℕ||hyps||
4. ↑mFOatomic?(hyps[i])
5. mFOatomic-name(hyps[i]) = "false" ∈ Atom
6. mFOatomic-vars(hyps[i]) = [] ∈ (ℤ List)
7. Dom : Type
8. S : FOStruct+{i:l}(Dom)
9. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
10. x : tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ x.i ∈ S "false" []

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List.  \mforall{}concl:mFOL().  \mforall{}i:\mBbbN{}||hyps||.
    ((\muparrow{}mFOatomic?(hyps[i]))
    {}\mRightarrow{}  (mFOatomic-name(hyps[i])  =  "false")
    {}\mRightarrow{}  (mFOatomic-vars(hyps[i])  =  [])
    {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(<hyps,  concl>))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``FOL-sequent-abstract  FOSatWith+``  0
  THEN  Fold  `FOSatWith+`  0
  THEN  UseWitness  \mkleeneopen{}\mlambda{}x.x.i\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SubsumeC    \mkleeneopen{}S  "false"  []\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index