Step
*
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;dl-sem(K;n.R[n];m.P[m]) prog(alpha);dl-sem(K;n.R[n];m.P'[m]) prog(alpha))
⊢ ∀k,k':K.  ([|alpha|] k k' 
⇐⇒ [|alpha|] k k')
BY
{ Folds ``dl-prog-sem dl-prop-sem`` (-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-same-sem(prog(alpha);K;[|alpha|];[|alpha|])
⊢ ∀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;dl-sem(K;n.R[n];m.P[m])  prog(alpha);dl-sem(K;n.R[n];m.P'[m]) 
                                                                                                                                  prog(alpha))
\mvdash{}  \mforall{}k,k':K.    ([|alpha|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k  k')
By
Latex:
Folds  ``dl-prog-sem  dl-prop-sem``  (-1)
Home
Index