---

Step * of Lemma consistent-context-model-stable

∀Gamma,more:mFOL() List. ∀M:mfol-context-model().
  (consistent-context-model(Gamma;M) ⇒ consistent-context-model(more @ Gamma;M))
BY
{ (Auto THEN D -2 THEN ParallelLast THEN All Reduce THEN RepeatFor 3 (ParallelLast) THEN EAuto 1) }

1
1. Gamma : mFOL() List
2. more : mFOL() List
3. M1 : (ℕ × Atom × ℕ × ℕ) List
4. M2 : (ℕ × ((ℕ × ℕ) List)) List
5. (∀c∈M1.consistent-model-const(Gamma;c))
6. ∀i:ℕ||M2||. let x,L = M2[i] in consistent-model-fun(Gamma;x;L)
7. i : ℕ||M2||
8. let x,L = M2[i] 
   in consistent-model-fun(Gamma;x;L)
⊢ let x,L = M2[i] 
  in consistent-model-fun(more @ Gamma;x;L)

---

Latex:

---

Latex:
\mforall{}Gamma,more:mFOL()  List.  \mforall{}M:mfol-context-model().
    (consistent-context-model(Gamma;M)  {}\mRightarrow{}  consistent-context-model(more  @  Gamma;M))


By

---

Latex:
(Auto  THEN  D  -2  THEN  ParallelLast  THEN  All  Reduce  THEN  RepeatFor  3  (ParallelLast)  THEN  EAuto  1)

---

Home Index