---

Step * of Lemma dl-program-eq-equiv

∀a,b:Prog.  equiv-props([(a ⇐⇒ b); (a ⇐⇒a b); (a ⇐⇒w b); a ≡ b])
BY
{ (Intros
   THEN (BLemma `implies-equiv-props` THENW Auto)
   THEN Reduce 0
   THEN RepUR ``last`` 0
   THEN (D 0 THENA Auto)
   THEN Try ((IntSegCases (-1) THEN Reduce 0 THEN (D 0 THENA Auto)))
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0) }

1
1. a : Prog
2. b : Prog
3. i : ℤ
4. i = 0 ∈ ℤ
5. ∀phi:Prop. (|= <a> phi ⇒ <b> phi ∧ |= <b> phi ⇒ <a> phi)
⊢ ∀p:ℕ. (|= <a> atm(p) ⇒ <b> atm(p) ∧ |= <b> atm(p) ⇒ <a> atm(p))

2
1. a : Prog
2. b : Prog
3. i : ℤ
4. i = 1 ∈ ℤ
5. ∀p:ℕ. (|= <a> atm(p) ⇒ <b> atm(p) ∧ |= <b> atm(p) ⇒ <a> atm(p))
⊢ ∃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))

3
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)

4
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)

---

Latex:

---

Latex:
\mforall{}a,b:Prog.    equiv-props([(a  \mLeftarrow{}{}\mRightarrow{}  b);  (a  \mLeftarrow{}{}\mRightarrow{}a  b);  (a  \mLeftarrow{}{}\mRightarrow{}w  b);  a  \mequiv{}  b])


By

---

Latex:
(Intros
  THEN  (BLemma  `implies-equiv-props`  THENW  Auto)
  THEN  Reduce  0
  THEN  RepUR  ``last``  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((IntSegCases  (-1)  THEN  Reduce  0  THEN  (D  0  THENA  Auto)))
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0)

---

Home Index