---

Step * of Lemma consistent-model-const-stable

∀Gamma,more:mFOL() List. ∀c:ℕ × Atom × ℕ × ℕ.
  (consistent-model-const(Gamma;c) ⇒ consistent-model-const(more @ Gamma;c))
BY
{ ((Auto THEN ParallelLast) THEN RepeatFor 3 (D -2) THEN All Reduce THEN D -1 THEN D 0) }

1
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||

2
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 

---

Latex:

---

Latex:
\mforall{}Gamma,more:mFOL()  List.  \mforall{}c:\mBbbN{}  \mtimes{}  Atom  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbN{}.
    (consistent-model-const(Gamma;c)  {}\mRightarrow{}  consistent-model-const(more  @  Gamma;c))


By

---

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

---

Home Index