---

Step * of Lemma pi-system-example_wf

     (Unhideable token semantics in effect)

∀[P:pi_term()]. (pi-system-example{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}(P) ∈ System(P.piM(P)))
BY
{ ProveWfLemma }

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 + Top

---

Latex:

---

Latex:
          (Unhideable  token  semantics  in  effect)

\mforall{}[P:pi\_term()].  (pi-system-example\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}(P)  \mmember{}  System(P.piM(P)))


By

---

Latex:
ProveWfLemma

---

Home Index