---

Step * 1 1 of Lemma wfd_tree_rec_node_lemma


1. F : Top@i
2. f : Top@i
3. F1 : Top@i
4. b : Top@i
⊢ F1[λb@0.W-rec(a,f,r.if a then b else F1[r] fi ;f b@0)] ~ F1[λx.wfd-tree-rec(b;r.F1[r];f x)]
BY
{ Try (RW (AddrC [2] (UnfoldC `wfd-tree-rec`⋅)) 0)⋅ }

1
1. F : Top@i
2. f : Top@i
3. F1 : Top@i
4. b : Top@i
⊢ F1[λb@0.W-rec(a,f,r.if a then b else F1[r] fi ;f b@0)] ~ F1[λx.W-rec(a,f,r.if a then b else F1[r] fi ;f x)]

---

Latex:

---

Latex:

1.  F  :  Top@i
2.  f  :  Top@i
3.  F1  :  Top@i
4.  b  :  Top@i
\mvdash{}  F1[\mlambda{}b@0.W-rec(a,f,r.if  a  then  b  else  F1[r]  fi  ;f  b@0)]  \msim{}  F1[\mlambda{}x.wfd-tree-rec(b;r.F1[r];f  x)]


By

---

Latex:
Try  (RW  (AddrC  [2]  (UnfoldC  `wfd-tree-rec`\mcdot{}))  0)\mcdot{}

---

Home Index