---

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


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())))
BY
{ (All (RepUR ``let``)
   THEN (ParallelLast THEN Auto)
   THEN OnMaybeHyp 8 (\h. (RepeatFor 2 (ParallelOp h)
                           THEN (MoveToConcl (-1) THEN (GenConclTerm ⌜L[i]⌝⋅ THENA Auto))
                           THEN D -2
                           THEN Reduce 0
                           THEN Auto))) }

---

Latex:

---

Latex:

1.  Gamma  :  mFOL()  List
2.  more  :  mFOL()  List
3.  x  :  \mBbbN{}
4.  L  :  (\mBbbN{}  \mtimes{}  \mBbbN{})  List
5.  x  <  ||Gamma||
6.  let  H  =  context-lookup(Gamma;x)  in
              ((\muparrow{}mFOquant?(H))
              \mwedge{}  mFOquant-isall(H)  =  tt
              \mwedge{}  (\mforall{}p\mmember{}L.let  i,j  =  p 
                              in  j  <  ||Gamma||  \mwedge{}  (mFOquant-body(H)[i/mFOquant-var(H)]  =  context-lookup(Gamma;j))))
              \mvee{}  ((\muparrow{}mFOconnect?(H))
                  \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "and"))
                  \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "or"))
                  \mwedge{}  (\mforall{}p\mmember{}L.let  i,j  =  p 
                                  in  i  <  ||Gamma||
                                        \mwedge{}  j  <  ||Gamma||
                                        \mwedge{}  (mFOconnect-left(H)  =  context-lookup(Gamma;i))
                                        \mwedge{}  (mFOconnect-right(H)  =  context-lookup(Gamma;j))))
\mvdash{}  let  H  =  context-lookup(Gamma;x)  in
            ((\muparrow{}mFOquant?(H))
            \mwedge{}  mFOquant-isall(H)  =  tt
            \mwedge{}  (\mforall{}p\mmember{}L.let  i,j  =  p 
                            in  j  <  ||more  @  Gamma||
                                  \mwedge{}  (mFOquant-body(H)[i/mFOquant-var(H)]  =  context-lookup(more  @  Gamma;j))))
            \mvee{}  ((\muparrow{}mFOconnect?(H))
                \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "and"))
                \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "or"))
                \mwedge{}  (\mforall{}p\mmember{}L.let  i,j  =  p 
                                in  i  <  ||more  @  Gamma||
                                      \mwedge{}  j  <  ||more  @  Gamma||
                                      \mwedge{}  (mFOconnect-left(H)  =  context-lookup(more  @  Gamma;i))
                                      \mwedge{}  (mFOconnect-right(H)  =  context-lookup(more  @  Gamma;j))))


By

---

Latex:
(All  (RepUR  ``let``)
  THEN  (ParallelLast  THEN  Auto)
  THEN  OnMaybeHyp  8  (\mbackslash{}h.  (RepeatFor  2  (ParallelOp  h)
                                                  THEN  (MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}L[i]\mkleeneclose{}\mcdot{}  THENA  Auto))
                                                  THEN  D  -2
                                                  THEN  Reduce  0
                                                  THEN  Auto)))

---

Home Index