---

Step * 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-same-sem(prog(alpha);K;[|alpha|];[|alpha|])
⊢ ∀k,k':K.  ([|alpha|] k k' ⇐⇒ [|alpha|] k k')
BY
{ D -1 }

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

---

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-same-sem(prog(alpha);K;[|alpha|];[|alpha|])
\mvdash{}  \mforall{}k,k':K.    ([|alpha|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k  k')


By

---

Latex:
D  -1

---

Home Index