---

Step * 2 of Lemma sdata-pair-has-atom


1. d1 : SecurityData
2. d2 : SecurityData
3. b : Atom1
4. b#<d1, d2>:SecurityData
⊢ b#d2:SecurityData
BY
{ (Subst ⌈d2 ~ if sdata-pair?(<d1, d2>) then sdata-right(<d1, d2>) else <d1, d2> fi ⌉ 0⋅
   THEN Try (FreeFromAtomApElim ⌈<d1, d2>⌉⋅)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  d1  :  SecurityData
2.  d2  :  SecurityData
3.  b  :  Atom1
4.  b\#<d1,  d2>:SecurityData
\mvdash{}  b\#d2:SecurityData


By

---

Latex:
(Subst  \mkleeneopen{}d2  \msim{}  if  sdata-pair?(<d1,  d2>)  then  sdata-right(<d1,  d2>)  else  <d1,  d2>  fi  \mkleeneclose{}  0\mcdot{}
  THEN  Try  (FreeFromAtomApElim  \mkleeneopen{}<d1,  d2>\mkleeneclose{}\mcdot{})
  THEN  Reduce  0
  THEN  Auto)

---

Home Index