---

Step * of Lemma ncomplete-test

No Annotations
((∀a:Prop. (localT prop(a) ∈ Prop List)) ∧ (∀n:node. (fst(n) ∈ Prop List)))
∧ (∀n:node. (∀f∈fst(n).f ∈ Prop))
∧ (∀n:node. (∀f1∈fst(n).(∀f∈localT prop(f1).f ∈ Prop)))
∧ (∀n:node. (∀f∈fst(n).(∀f1∈localT prop(f).(∃f1'∈fst(n). dlo_eq(prop(f1);prop(f1')) ∈ 𝔹))))
BY
{ Auto }

1
1. ∀a:Prop. (localT prop(a) ∈ Prop List)
2. ∀n:node. (fst(n) ∈ Prop List)
3. n : node
⊢ (∀f∈fst(n).f ∈ Prop)

2
1. ∀a:Prop. (localT prop(a) ∈ Prop List)
2. ∀n:node. (fst(n) ∈ Prop List)
3. ∀n:node. (∀f∈fst(n).f ∈ Prop)
4. n : node
⊢ (∀f1∈fst(n).(∀f∈localT prop(f1).f ∈ Prop))

3
1. ∀a:Prop. (localT prop(a) ∈ Prop List)
2. ∀n:node. (fst(n) ∈ Prop List)
3. ∀n:node. (∀f∈fst(n).f ∈ Prop)
4. ∀n:node. (∀f1∈fst(n).(∀f∈localT prop(f1).f ∈ Prop))
5. n : node
⊢ (∀f∈fst(n).(∀f1∈localT prop(f).(∃f1'∈fst(n). dlo_eq(prop(f1);prop(f1')) ∈ 𝔹)))

---

Latex:

---

Latex:
No  Annotations
((\mforall{}a:Prop.  (localT  prop(a)  \mmember{}  Prop  List))  \mwedge{}  (\mforall{}n:node.  (fst(n)  \mmember{}  Prop  List)))
\mwedge{}  (\mforall{}n:node.  (\mforall{}f\mmember{}fst(n).f  \mmember{}  Prop))
\mwedge{}  (\mforall{}n:node.  (\mforall{}f1\mmember{}fst(n).(\mforall{}f\mmember{}localT  prop(f1).f  \mmember{}  Prop)))
\mwedge{}  (\mforall{}n:node.  (\mforall{}f\mmember{}fst(n).(\mforall{}f1\mmember{}localT  prop(f).(\mexists{}f1'\mmember{}fst(n).  dlo\_eq(prop(f1);prop(f1'))  \mmember{}  \mBbbB{}))))


By

---

Latex:
Auto

---

Home Index