---

Step * 1 of Lemma consistent-context-model-stable


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)
BY
{ (MoveToConcl (-1) THEN (GenConclTerm ⌜M2[i]⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  Gamma  :  mFOL()  List
2.  more  :  mFOL()  List
3.  M1  :  (\mBbbN{}  \mtimes{}  Atom  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbN{})  List
4.  M2  :  (\mBbbN{}  \mtimes{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List))  List
5.  (\mforall{}c\mmember{}M1.consistent-model-const(Gamma;c))
6.  \mforall{}i:\mBbbN{}||M2||.  let  x,L  =  M2[i]  in  consistent-model-fun(Gamma;x;L)
7.  i  :  \mBbbN{}||M2||
8.  let  x,L  =  M2[i] 
      in  consistent-model-fun(Gamma;x;L)
\mvdash{}  let  x,L  =  M2[i] 
    in  consistent-model-fun(more  @  Gamma;x;L)


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}M2[i]\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  EAuto  1)

---

Home Index