---

Step * 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')
⊢ ∀k,k':K.  (([|x|]^*) k k' ⇐⇒ ([|x|]^*) k k')
BY
{ ((InstLemma `rel_star_functionality_wrt_rel_implies` [⌜K⌝;⌜[|x|]⌝;⌜[|x|]⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
   THEN (InstLemma `rel_star_functionality_wrt_rel_implies` [⌜K⌝;⌜[|x|]⌝;⌜[|x|]⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
   ) }

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

---

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')
\mvdash{}  \mforall{}k,k':K.    (rel\_star(K;  [|x|])  k  k'  \mLeftarrow{}{}\mRightarrow{}  rel\_star(K;  [|x|])  k  k')


By

---

Latex:
((InstLemma  `rel\_star\_functionality\_wrt\_rel\_implies`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}[|x|]\mkleeneclose{};\mkleeneopen{}[|x|]\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  D  0  THEN  Auto)
    )
  THEN  (InstLemma  `rel\_star\_functionality\_wrt\_rel\_implies`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}[|x|]\mkleeneclose{};\mkleeneopen{}[|x|]\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Auto)
              )
  )

---

Home Index