---

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


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)) = "prog" ∈ Atom) ⇒ (∀k,k':K.  ([|alpha|] k k' ⇐⇒ [|alpha|] k k'))
8. (dl-kind(prog(alpha)) = "prop" ∈ Atom) ⇒ (∀k:K. ([|alpha|] k ⇐⇒ [|alpha|] k))
⊢ ∀k,k':K.  ([|alpha|] k k' ⇐⇒ [|alpha|] k k')
BY
{ (D -2 THEN Try (Trivial)) }

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

---

Latex:

---

Latex:

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))  =  "prog")  {}\mRightarrow{}  (\mforall{}k,k':K.    ([|alpha|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k  k'))
8.  (dl-kind(prog(alpha))  =  "prop")  {}\mRightarrow{}  (\mforall{}k:K.  ([|alpha|]  k  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k))
\mvdash{}  \mforall{}k,k':K.    ([|alpha|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k  k')


By

---

Latex:
(D  -2  THEN  Try  (Trivial))

---

Home Index