---

Step * 1 of Lemma dl-valid-box-comp-double-box2


1. a : Prog
2. b : Prog
3. phi : Prop
4. ∀K:Type. ∀R:Atom ⟶ K ⟶ K ⟶ ℙ. ∀P:Atom ⟶ K ⟶ ℙ. ∀k:K.  ((snd(dl-sem(K;n.R[n];m.P[m]))) [a] [b] phi k)
5. K : Type
6. R : Atom ⟶ K ⟶ K ⟶ ℙ
7. P : Atom ⟶ K ⟶ ℙ
8. k : K
9. ∀k':K
     (((fst(dl-sem(K;n.R[n];m.P[m]))) a k k')
     ⇒ (∀k'@0:K. (((fst(dl-sem(K;n.R[n];m.P[m]))) b k' k'@0) ⇒ ((snd(dl-sem(K;n.R[n];m.P[m]))) phi k'@0))))
10. k' : K
11. ∃k2:K. (((fst(dl-sem(K;n.R[n];m.P[m]))) a k k2) ∧ ((fst(dl-sem(K;n.R[n];m.P[m]))) b k2 k'))
⊢ (snd(dl-sem(K;n.R[n];m.P[m]))) phi k'
BY
{ (ExRepD THEN InstHyp [⌜k2⌝;⌜k'⌝] (9)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Prog
2.  b  :  Prog
3.  phi  :  Prop
4.  \mforall{}K:Type.  \mforall{}R:Atom  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}P:Atom  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}k:K.
          ((snd(dl-sem(K;n.R[n];m.P[m])))  [a]  [b]  phi  k)
5.  K  :  Type
6.  R  :  Atom  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
7.  P  :  Atom  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
8.  k  :  K
9.  \mforall{}k':K
          (((fst(dl-sem(K;n.R[n];m.P[m])))  a  k  k')
          {}\mRightarrow{}  (\mforall{}k'@0:K
                      (((fst(dl-sem(K;n.R[n];m.P[m])))  b  k'  k'@0)
                      {}\mRightarrow{}  ((snd(dl-sem(K;n.R[n];m.P[m])))  phi  k'@0))))
10.  k'  :  K
11.  \mexists{}k2:K.  (((fst(dl-sem(K;n.R[n];m.P[m])))  a  k  k2)  \mwedge{}  ((fst(dl-sem(K;n.R[n];m.P[m])))  b  k2  k'))
\mvdash{}  (snd(dl-sem(K;n.R[n];m.P[m])))  phi  k'


By

---

Latex:
(ExRepD  THEN  InstHyp  [\mkleeneopen{}k2\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{}]  (9)\mcdot{}  THEN  Auto)

---

Home Index