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] ⇐⇒ 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' ⇐⇒ [|alpha|] 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] ⇐⇒ P'[n] k))
7. dl-same-sem(prog(alpha);K;[|alpha|];[|alpha|])
⊢ ∀k,k':K.  ([|alpha|] k' ⇐⇒ [|alpha|] 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