---

Step * 1 of Lemma pi-system-example_wf


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

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

2
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)

---

Latex:

---

Latex:

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


By

---

Latex:
SubsumeC  \mkleeneopen{}Id?\mkleeneclose{}\mcdot{}

---

Home Index