---

Step * 1 of Lemma wfd_tree_rec_node_lemma


1. F : Top@i
2. f : Top@i
3. F1 : Top@i
4. b : Top@i
⊢ wfd-tree-rec(b;r.F1[r];Wsup(ff;f)) ~ F1[λx.wfd-tree-rec(b;r.F1[r];f x)]
BY
{ Try (RW (AddrC [1] (UnfoldC `wfd-tree-rec` ANDTHENC RecUnfoldC `W-rec` ANDTHENC (TagC (mk_tag_term 5)))) 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.wfd-tree-rec(b;r.F1[r];f x)]

---

Latex:

---

Latex:

1.  F  :  Top@i
2.  f  :  Top@i
3.  F1  :  Top@i
4.  b  :  Top@i
\mvdash{}  wfd-tree-rec(b;r.F1[r];Wsup(ff;f))  \msim{}  F1[\mlambda{}x.wfd-tree-rec(b;r.F1[r];f  x)]


By

---

Latex:
Try  (RW  (AddrC  [1]  (
UnfoldC  `wfd-tree-rec`  ANDTHENC  RecUnfoldC  `W-rec`  ANDTHENC  (TagC  (mk\_tag\_term  5))))  0)\mcdot{}

---

Home Index