---

Step * of Lemma consistent-model-fun-stable

No Annotations
∀Gamma,more:mFOL() List. ∀x:ℕ. ∀L:(ℕ × ℕ) List.
  (consistent-model-fun(Gamma;x;L) ⇒ consistent-model-fun(more @ Gamma;x;L))
BY
{ (Auto
   THEN ParallelLast
   THEN D -1
   THEN (D 0 THEN Try (Complete (Auto)))
   THEN (Subst' context-lookup(more @ Gamma;x) ~ context-lookup(Gamma;x) 0 THENA Auto)) }

1
1. Gamma : mFOL() List
2. more : mFOL() List
3. x : ℕ
4. L : (ℕ × ℕ) List
5. x < ||Gamma||
6. let H = context-lookup(Gamma;x) in
       ((↑mFOquant?(H))
       ∧ mFOquant-isall(H) = tt
       ∧ (∀p∈L.let i,j = p 
               in j < ||Gamma|| ∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(Gamma;j) ∈ mFOL())))
       ∨ ((↑mFOconnect?(H))
         ∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom))
         ∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom))
         ∧ (∀p∈L.let i,j = p 
                 in i < ||Gamma||
                    ∧ j < ||Gamma||
                    ∧ (mFOconnect-left(H) = context-lookup(Gamma;i) ∈ mFOL())
                    ∧ (mFOconnect-right(H) = context-lookup(Gamma;j) ∈ mFOL())))
⊢ let H = context-lookup(Gamma;x) in
      ((↑mFOquant?(H))
      ∧ mFOquant-isall(H) = tt
      ∧ (∀p∈L.let i,j = p 
              in j < ||more @ Gamma||
                 ∧ (mFOquant-body(H)[i/mFOquant-var(H)] = context-lookup(more @ Gamma;j) ∈ mFOL())))
      ∨ ((↑mFOconnect?(H))
        ∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom))
        ∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom))
        ∧ (∀p∈L.let i,j = p 
                in i < ||more @ Gamma||
                   ∧ j < ||more @ Gamma||
                   ∧ (mFOconnect-left(H) = context-lookup(more @ Gamma;i) ∈ mFOL())
                   ∧ (mFOconnect-right(H) = context-lookup(more @ Gamma;j) ∈ mFOL())))

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma,more:mFOL()  List.  \mforall{}x:\mBbbN{}.  \mforall{}L:(\mBbbN{}  \mtimes{}  \mBbbN{})  List.
    (consistent-model-fun(Gamma;x;L)  {}\mRightarrow{}  consistent-model-fun(more  @  Gamma;x;L))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  D  -1
  THEN  (D  0  THEN  Try  (Complete  (Auto)))
  THEN  (Subst'  context-lookup(more  @  Gamma;x)  \msim{}  context-lookup(Gamma;x)  0  THENA  Auto))

---

Home Index