---

Step * of Lemma dl-prog-sem_functionality

∀alpha:Prog
  ∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
    ((∀n∈dl-prop-atoms() prog(alpha).∀k:K. (P[n] k ⇐⇒ P'[n] k)) ⇒ (∀k,k':K.  ([|alpha|] k k' ⇐⇒ [|alpha|] k k')))
BY
{ ((D 0 THENA Auto) THEN (InstLemma `dl-sem_functionality1` [⌜prog(alpha)⌝]⋅ THENA Auto)) }

1
1. alpha : Prog
2. ∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
     ((∀n∈dl-prop-atoms() prog(alpha).∀k:K. (P[n] k ⇐⇒ P'[n] k))
     ⇒ 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:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
    ((∀n∈dl-prop-atoms() prog(alpha).∀k:K. (P[n] k ⇐⇒ P'[n] k)) ⇒ (∀k,k':K.  ([|alpha|] k k' ⇐⇒ [|alpha|] k k')))

---

Latex:

---

Latex:
\mforall{}alpha:Prog
    \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(alpha).\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
        {}\mRightarrow{}  (\mforall{}k,k':K.    ([|alpha|]  k  k'  \mLeftarrow{}{}\mRightarrow{}  [|alpha|]  k  k')))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstLemma  `dl-sem\_functionality1`  [\mkleeneopen{}prog(alpha)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index