---

Step * 1 2 of Lemma pi-system-example_wf


1. P : pi_term()
2. l : Id List@i
3. apply-alist(NatDeq;ten-locs{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}();||l|| + 4)
= apply-alist(NatDeq;ten-locs{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}();||l|| + 4)
∈ (Id?)
⊢ (Id?) ⊆r (Id + Top)
BY
{ Auto }

---

Latex:

---

Latex:

1.  P  :  pi\_term()
2.  l  :  Id  List@i
3.  apply-alist(NatDeq;ten-locs\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}();||l||  +  4)
=  apply-alist(NatDeq;ten-locs\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}();||l||  +  4)
\mvdash{}  (Id?)  \msubseteq{}r  (Id  +  Top)


By

---

Latex:
Auto

---

Home Index