---

Step * 2 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 
⊢ let H = context-lookup(more @ 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 < ||more @ Gamma||
             ∧ c6 < ||more @ Gamma||
             ∧ (↑mFOconnect?(H))
             ∧ (mFOconnect-knd(H) = "and" ∈ Atom)
             ∧ (mFOconnect-left(H) = context-lookup(more @ Gamma;c5) ∈ mFOL())
             ∧ (mFOconnect-right(H) = context-lookup(more @ Gamma;c6) ∈ mFOL())
      if c3 =a "dpair"
        then c6 < ||more @ Gamma||
             ∧ (↑mFOquant?(H))
             ∧ mFOquant-isall(H) = ff
             ∧ (mFOquant-body(H)[c5/mFOquant-var(H)] = context-lookup(more @ Gamma;c6) ∈ mFOL())
      if c3 =a "inl"
        then c5 < ||more @ Gamma||
             ∧ (↑mFOconnect?(H))
             ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
             ∧ (mFOconnect-left(H) = context-lookup(more @ Gamma;c5) ∈ mFOL())
      if c3 =a "inr"
        then c5 < ||more @ Gamma||
             ∧ (↑mFOconnect?(H))
             ∧ (mFOconnect-knd(H) = "or" ∈ Atom)
             ∧ (mFOconnect-right(H) = context-lookup(more @ Gamma;c5) ∈ mFOL())
      else True
      fi 
BY
{ ((Subst' context-lookup(more @ Gamma;c1) ~ context-lookup(Gamma;c1) 0 THENA Auto)
   THEN (MoveToConcl (-1) THEN (GenConclTerm ⌜context-lookup(Gamma;c1)⌝⋅ THENA Auto))
   THEN RepUR ``let`` 0
   THEN Repeat (AutoSplit)) }

---

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{}  let  H  =  context-lookup(more  @  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  <  ||more  @  Gamma||
                          \mwedge{}  c6  <  ||more  @  Gamma||
                          \mwedge{}  (\muparrow{}mFOconnect?(H))
                          \mwedge{}  (mFOconnect-knd(H)  =  "and")
                          \mwedge{}  (mFOconnect-left(H)  =  context-lookup(more  @  Gamma;c5))
                          \mwedge{}  (mFOconnect-right(H)  =  context-lookup(more  @  Gamma;c6))
            if  c3  =a  "dpair"
                then  c6  <  ||more  @  Gamma||
                          \mwedge{}  (\muparrow{}mFOquant?(H))
                          \mwedge{}  mFOquant-isall(H)  =  ff
                          \mwedge{}  (mFOquant-body(H)[c5/mFOquant-var(H)]  =  context-lookup(more  @  Gamma;c6))
            if  c3  =a  "inl"
                then  c5  <  ||more  @  Gamma||
                          \mwedge{}  (\muparrow{}mFOconnect?(H))
                          \mwedge{}  (mFOconnect-knd(H)  =  "or")
                          \mwedge{}  (mFOconnect-left(H)  =  context-lookup(more  @  Gamma;c5))
            if  c3  =a  "inr"
                then  c5  <  ||more  @  Gamma||
                          \mwedge{}  (\muparrow{}mFOconnect?(H))
                          \mwedge{}  (mFOconnect-knd(H)  =  "or")
                          \mwedge{}  (mFOconnect-right(H)  =  context-lookup(more  @  Gamma;c5))
            else  True
            fi 


By

---

Latex:
((Subst'  context-lookup(more  @  Gamma;c1)  \msim{}  context-lookup(Gamma;c1)  0  THENA  Auto)
  THEN  (MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}context-lookup(Gamma;c1)\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  RepUR  ``let``  0
  THEN  Repeat  (AutoSplit))

---

Home Index