---

Step * of Lemma assert-dlo_eq

∀a,b:dl-Obj().  (↑dlo_eq(a;b) ⇐⇒ a = b ∈ dl-Obj())
BY
{ (dlObjInduction THEN Intros THEN MoveToConcl (-1)) }

1
1. x : ℕ
⊢ ∀b:dl-Obj(). (↑dlo_eq(prog(atm(x));b) ⇐⇒ prog(atm(x)) = b ∈ dl-Obj())

2
1. x : Prog
2. x1 : Prog
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prog(x1);b) ⇐⇒ prog(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prog((x;x1));b) ⇐⇒ prog((x;x1)) = b ∈ dl-Obj())

3
1. x : Prog
2. x1 : Prog
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prog(x1);b) ⇐⇒ prog(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prog(x ⋃ x1);b) ⇐⇒ prog(x ⋃ x1) = b ∈ dl-Obj())

4
1. x : Prog
2. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prog((x)*);b) ⇐⇒ prog((x)*) = b ∈ dl-Obj())

5
1. x : Prop
2. ∀b:dl-Obj(). (↑dlo_eq(prop(x);b) ⇐⇒ prop(x) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prog((x)?);b) ⇐⇒ prog((x)?) = b ∈ dl-Obj())

6
1. x : ℕ
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop(atm(x));b) ⇐⇒ prop(atm(x)) = b ∈ dl-Obj())

7
∀b:dl-Obj(). (↑dlo_eq(prop(0);b) ⇐⇒ prop(0) = b ∈ dl-Obj())

8
1. x : Prop
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prop(x);b) ⇐⇒ prop(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop(x ⇒ x1);b) ⇐⇒ prop(x ⇒ x1) = b ∈ dl-Obj())

9
1. x : Prop
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prop(x);b) ⇐⇒ prop(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop(x ∧ x1);b) ⇐⇒ prop(x ∧ x1) = b ∈ dl-Obj())

10
1. x : Prop
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prop(x);b) ⇐⇒ prop(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop(x ∨ x1);b) ⇐⇒ prop(x ∨ x1) = b ∈ dl-Obj())

11
1. x : Prog
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop([x] x1);b) ⇐⇒ prop([x] x1) = b ∈ dl-Obj())

12
1. x : Prog
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
⊢ ∀b:dl-Obj(). (↑dlo_eq(prop(<x> x1);b) ⇐⇒ prop(<x> x1) = b ∈ dl-Obj())

---

Latex:

---

Latex:
\mforall{}a,b:dl-Obj().    (\muparrow{}dlo\_eq(a;b)  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
(dlObjInduction  THEN  Intros  THEN  MoveToConcl  (-1))

---

Home Index