---

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


1. Gamma : mFOL() List
2. more : mFOL() List
3. c1 : ℕ
4. c3 : Atom
5. c5 : ℕ
6. c6 : ℕ
7. c1 < ||Gamma||
8. let H = context-lookup(Gamma;c1) in
       if c3 =a "function"
         then ((↑mFOconnect?(H)) ∧ (¬(mFOconnect-knd(H) = "and" ∈ Atom)) ∧ (¬(mFOconnect-knd(H) = "or" ∈ Atom)))
              ∨ ((↑mFOquant?(H)) ∧ mFOquant-isall(H) = tt)
       if c3 =a "pair"
         then c5 < ||Gamma||
              ∧ c6 < ||Gamma||
              ∧ (↑mFOconnect?(H))
              ∧ (mFOconnect-knd(H) = "and" ∈ Atom)
              ∧ (mFOconnect-left(H) = context-lookup(Gamma;c5) ∈ mFOL())
              ∧ (mFOconnect-right(H) = context-lookup(Gamma;c6) ∈ mFOL())
       if c3 =a "dpair"
         then c6 < ||Gamma||
              ∧ (↑mFOquant?(H))
              ∧ mFOquant-isall(H) = ff
              ∧ (mFOquant-body(H)[c5/mFOquant-var(H)] = context-lookup(Gamma;c6) ∈ mFOL())
       if c3 =a "inl"
         then c5 < ||Gamma||
              ∧ (↑mFOconnect?(H))
              ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
              ∧ (mFOconnect-left(H) = context-lookup(Gamma;c5) ∈ mFOL())
       if c3 =a "inr"
         then c5 < ||Gamma||
              ∧ (↑mFOconnect?(H))
              ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
              ∧ (mFOconnect-right(H) = context-lookup(Gamma;c5) ∈ mFOL())
       else True
       fi 
⊢ c1 < ||more @ Gamma||
BY
{ (Thin (-1) THEN Auto') }

---

Latex:

---

Latex:

1.  Gamma  :  mFOL()  List
2.  more  :  mFOL()  List
3.  c1  :  \mBbbN{}
4.  c3  :  Atom
5.  c5  :  \mBbbN{}
6.  c6  :  \mBbbN{}
7.  c1  <  ||Gamma||
8.  let  H  =  context-lookup(Gamma;c1)  in
              if  c3  =a  "function"
                  then  ((\muparrow{}mFOconnect?(H))  \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "and"))  \mwedge{}  (\mneg{}(mFOconnect-knd(H)  =  "or")))
                            \mvee{}  ((\muparrow{}mFOquant?(H))  \mwedge{}  mFOquant-isall(H)  =  tt)
              if  c3  =a  "pair"
                  then  c5  <  ||Gamma||
                            \mwedge{}  c6  <  ||Gamma||
                            \mwedge{}  (\muparrow{}mFOconnect?(H))
                            \mwedge{}  (mFOconnect-knd(H)  =  "and")
                            \mwedge{}  (mFOconnect-left(H)  =  context-lookup(Gamma;c5))
                            \mwedge{}  (mFOconnect-right(H)  =  context-lookup(Gamma;c6))
              if  c3  =a  "dpair"
                  then  c6  <  ||Gamma||
                            \mwedge{}  (\muparrow{}mFOquant?(H))
                            \mwedge{}  mFOquant-isall(H)  =  ff
                            \mwedge{}  (mFOquant-body(H)[c5/mFOquant-var(H)]  =  context-lookup(Gamma;c6))
              if  c3  =a  "inl"
                  then  c5  <  ||Gamma||
                            \mwedge{}  (\muparrow{}mFOconnect?(H))
                            \mwedge{}  (mFOconnect-knd(H)  =  "or")
                            \mwedge{}  (mFOconnect-left(H)  =  context-lookup(Gamma;c5))
              if  c3  =a  "inr"
                  then  c5  <  ||Gamma||
                            \mwedge{}  (\muparrow{}mFOconnect?(H))
                            \mwedge{}  (mFOconnect-knd(H)  =  "or")
                            \mwedge{}  (mFOconnect-right(H)  =  context-lookup(Gamma;c5))
              else  True
              fi 
\mvdash{}  c1  <  ||more  @  Gamma||


By

---

Latex:
(Thin  (-1)  THEN  Auto')

---

Home Index