---

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


1. a : Prog
2. b : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. ∃p:ℕ
    ((¬(p ∈ dl-prop-atoms() prog(a)))
    ∧ (¬(p ∈ dl-prop-atoms() prog(b)))
    ∧ |= <a> atm(p) ⇒ <b> atm(p)
    ∧ |= <b> atm(p) ⇒ <a> atm(p))
⊢ ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k1,k2:K.  ([|a|] k1 k2 ⇐⇒ [|b|] k1 k2)
BY
{ ((ExRepD THENA Auto)
   THEN (Assert λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ BY
               Auto)
   THEN All (RepUR ``dl-valid``)
   THEN Auto) }

1
1. a : Prog
2. b : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. p : ℕ
6. ¬(p ∈ dl-prop-atoms() prog(a))
7. ¬(p ∈ dl-prop-atoms() prog(b))
8. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<a> atm(p) ⇒ <b> atm(p)|] k)
9. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<b> atm(p) ⇒ <a> atm(p)|] k)
10. K : Type
11. R : ℕ ⟶ K ⟶ K ⟶ ℙ
12. P : ℕ ⟶ K ⟶ ℙ
13. k1 : K
14. k2 : K
15. λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ
16. [|a|] k1 k2
⊢ [|b|] k1 k2

2
1. a : Prog
2. b : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. p : ℕ
6. ¬(p ∈ dl-prop-atoms() prog(a))
7. ¬(p ∈ dl-prop-atoms() prog(b))
8. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<a> atm(p) ⇒ <b> atm(p)|] k)
9. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<b> atm(p) ⇒ <a> atm(p)|] k)
10. K : Type
11. R : ℕ ⟶ K ⟶ K ⟶ ℙ
12. P : ℕ ⟶ K ⟶ ℙ
13. k1 : K
14. k2 : K
15. λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ
16. [|b|] k1 k2
⊢ [|a|] k1 k2

---

Latex:

---

Latex:

1.  a  :  Prog
2.  b  :  Prog
3.  i  :  \mBbbZ{}
4.  i  =  2
5.  \mexists{}p:\mBbbN{}
        ((\mneg{}(p  \mmember{}  dl-prop-atoms()  prog(a)))
        \mwedge{}  (\mneg{}(p  \mmember{}  dl-prop-atoms()  prog(b)))
        \mwedge{}  |=  <a>  atm(p)  {}\mRightarrow{}  <b>  atm(p)
        \mwedge{}  |=  <b>  atm(p)  {}\mRightarrow{}  <a>  atm(p))
\mvdash{}  \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)


By

---

Latex:
((ExRepD  THENA  Auto)
  THEN  (Assert  \mlambda{}\msubtwo{}a.\mlambda{}s.if  (a  =\msubz{}  p)  then  s  =  k2  else  P  a  s  fi    \mmember{}  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}  BY
                          Auto)
  THEN  All  (RepUR  ``dl-valid``)
  THEN  Auto)

---

Home Index