---

Step * 4 of Lemma dl-program-eq-equiv


1. a : Prog
2. b : Prog
3. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k1,k2:K.  ([|a|] k1 k2 ⇐⇒ [|b|] k1 k2)
⊢ ∀phi:Prop. (|= <a> phi ⇒ <b> phi ∧ |= <b> phi ⇒ <a> phi)
BY
{ (RepeatFor 6 ((D 0 THENA Auto)) THEN DlSemReduce 0 THEN RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Prog
2.  b  :  Prog
3.  \mforall{}K:Type.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}k1,k2:K.    ([|a|]  k1  k2  \mLeftarrow{}{}\mRightarrow{}  [|b|]  k1  k2)
\mvdash{}  \mforall{}phi:Prop.  (|=  <a>  phi  {}\mRightarrow{}  <b>  phi  \mwedge{}  |=  <b>  phi  {}\mRightarrow{}  <a>  phi)


By

---

Latex:
(RepeatFor  6  ((D  0  THENA  Auto))  THEN  DlSemReduce  0  THEN  RWO  "3"  0  THEN  Auto)

---

Home Index