---

Step * 1 1 1 1 1 of Lemma dl-prog-sem_functionality

.....antecedent..... 
1. alpha : Prog
2. K : Type
3. R : ℕ ⟶ K ⟶ K ⟶ ℙ
4. P : ℕ ⟶ K ⟶ ℙ
5. P' : ℕ ⟶ K ⟶ ℙ
6. (∀n∈dl-prop-atoms() prog(alpha).∀k:K. (P[n] k ⇐⇒ P'[n] k))
7. (dl-kind(prog(alpha)) = "prop" ∈ Atom) ⇒ (∀k:K. ([|alpha|] k ⇐⇒ [|alpha|] k))
⊢ dl-kind(prog(alpha)) = "prog" ∈ Atom
BY
{ (Computation THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  alpha  :  Prog
2.  K  :  Type
3.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
4.  P  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  P'  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
6.  (\mforall{}n\mmember{}dl-prop-atoms()  prog(alpha).\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
7.  (dl-kind(prog(alpha))  =  "prop")  {}\mRightarrow{}  (\mforall{}k:K.  ([|alpha|]  k  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k))
\mvdash{}  dl-kind(prog(alpha))  =  "prog"


By

---

Latex:
(Computation  THEN  Auto)

---

Home Index