---

Step * 1 of Lemma st-atom-encrypt


1. T : Id ─→ Type
2. K : ℕ
3. t2 : ℕ
4. t3 : ℕK ─→ (Atom1 × ℕ + Atom1 × data(T))
5. k1 : ℕ + Atom1
6. k2 : data(T)
7. n : ℕK
8. t2 < K
⊢ (fst(((λy.if (y =z t2) then <fst((t3 t2)), k1, k2> else t3 y fi ) n))) = (fst((t3 n))) ∈ Atom1
BY
{ (Reduce 0 THEN SplitOnConclITE THEN Reduce 0 THEN Auto THEN (HypSubst' (-1) 0) THEN Auto)⋅ }

---

Latex:



1.  T  :  Id  {}\mrightarrow{}  Type
2.  K  :  \mBbbN{}
3.  t2  :  \mBbbN{}
4.  t3  :  \mBbbN{}K  {}\mrightarrow{}  (Atom1  \mtimes{}  \mBbbN{}  +  Atom1  \mtimes{}  data(T))
5.  k1  :  \mBbbN{}  +  Atom1
6.  k2  :  data(T)
7.  n  :  \mBbbN{}K
8.  t2  <  K
\mvdash{}  (fst(((\mlambda{}y.if  (y  =\msubz{}  t2)  then  <fst((t3  t2)),  k1,  k2>  else  t3  y  fi  )  n)))  =  (fst((t3  n)))


By

(Reduce  0  THEN  SplitOnConclITE  THEN  Reduce  0  THEN  Auto  THEN  (HypSubst'  (-1)  0)  THEN  Auto)\mcdot{}

---

Home Index