---

Step * 1 1 of Lemma dl-sem_functionality1


1. x : Prog
2. ∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
     ((∀n∈dl-prop-atoms() prog(x).∀k:K. (P[n] k ⇐⇒ P'[n] k)) ⇒ dl-same-sem(prog(x);K;[|x|];[|x|]))
3. [K] : Type
4. [R] : ℕ ⟶ K ⟶ K ⟶ ℙ
5. [P] : ℕ ⟶ K ⟶ ℙ
6. [P'] : ℕ ⟶ K ⟶ ℙ
7. (∀n∈dl-prop-atoms() prog((x)*).∀k:K. (P[n] k ⇐⇒ P'[n] k))
8. dl-kind(prog((x)*)) = "prog" ∈ Atom
9. ∀k,k':K.  ([|x|] k k' ⇐⇒ [|x|] k k')
10. [|x|]^* => [|x|]^*
11. [|x|]^* => [|x|]^*
⊢ ∀k,k':K.  (([|x|]^*) k k' ⇐⇒ ([|x|]^*) k k')
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  Prog
2.  \mforall{}[K:Type].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P,P':\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].
          ((\mforall{}n\mmember{}dl-prop-atoms()  prog(x).\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))  {}\mRightarrow{}  dl-same-sem(prog(x);K;[|x|];[|x|]))
3.  [K]  :  Type
4.  [R]  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  [P]  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
6.  [P']  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
7.  (\mforall{}n\mmember{}dl-prop-atoms()  prog((x)*).\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
8.  dl-kind(prog((x)*))  =  "prog"
9.  \mforall{}k,k':K.    ([|x|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|x|]  k  k')
10.  rel\_star(K;  [|x|])  =>  rel\_star(K;  [|x|])
11.  rel\_star(K;  [|x|])  =>  rel\_star(K;  [|x|])
\mvdash{}  \mforall{}k,k':K.    (rel\_star(K;  [|x|])  k  k'  \mLeftarrow{}{}\mRightarrow{}  rel\_star(K;  [|x|])  k  k')


By

---

Latex:
Auto

---

Home Index