---

Step * of Lemma sdata-pair-has-atom

∀[d1,d2:SecurityData]. ∀[b:Atom1].  uiff(b#<d1, d2>:SecurityData;b#d1:SecurityData ∧ b#d2:SecurityData)
BY
{ Auto }

1
1. d1 : SecurityData
2. d2 : SecurityData
3. b : Atom1
4. b#<d1, d2>:SecurityData
⊢ b#d1:SecurityData

2
1. d1 : SecurityData
2. d2 : SecurityData
3. b : Atom1
4. b#<d1, d2>:SecurityData
⊢ b#d2:SecurityData

3
1. d1 : SecurityData
2. d2 : SecurityData
3. b : Atom1
4. b#d1:SecurityData
5. b#d2:SecurityData
⊢ b#<d1, d2>:SecurityData

---

Latex:

---

Latex:
\mforall{}[d1,d2:SecurityData].  \mforall{}[b:Atom1].
    uiff(b\#<d1,  d2>:SecurityData;b\#d1:SecurityData  \mwedge{}  b\#d2:SecurityData)


By

---

Latex:
Auto

---

Home Index