---

Step * of Lemma rank-pi-choices

∀[P:pi_term()]. ∀[choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(P))} ].  pi-rank(snd(choice)) < pi-rank(P)
BY
{ (RemoveUniform Auto Auto
   THEN (BLemma `pi_term-induction` THENA Auto)
   THEN Unfolds ``pi-choices pi-rank`` 0⋅
   THEN Reduce 0
   THEN Try (Folds ``pi-choices pi-rank`` 0)
   THEN (Auto THEN AllHyps h.DSet h  THEN AllHyps h.(RWO "nil_member member_singleton member_append" h⋅ THEN Auto) )⋅) }

1
1. pre : pi_prefix()@i
2. body : pi_term()@i
3. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(body))} . pi-rank(snd(choice)) < pi-rank(body)@i
4. choice : pi_prefix() × pi_term()@i
5. choice = <pre, body> ∈ (pi_prefix() × pi_term())
⊢ pi-rank(snd(choice)) < pi-rank(body) + 1

2
1. left : pi_term()@i
2. right : pi_term()@i
3. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(left))} . pi-rank(snd(choice)) < pi-rank(left)@i
4. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(right))} . pi-rank(snd(choice)) < pi-rank(right)@i
5. choice : pi_prefix() × pi_term()@i
6. (choice ∈ pi-choices(left)) ∨ (choice ∈ pi-choices(right))
⊢ pi-rank(snd(choice)) < pi-rank(left) + pi-rank(right) + 1

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()].  \mforall{}[choice:\{c:pi\_prefix()  \mtimes{}  pi\_term()|  (c  \mmember{}  pi-choices(P))\}  ].
    pi-rank(snd(choice))  <  pi-rank(P)


By

---

Latex:
(RemoveUniform  Auto  Auto
  THEN  (BLemma  `pi\_term-induction`  THENA  Auto)
  THEN  Unfolds  ``pi-choices  pi-rank``  0\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Folds  ``pi-choices  pi-rank``  0)
  THEN  (Auto
              THEN  AllHyps  h.DSet  h 
              THEN  AllHyps  h.(RWO  "nil\_member  member\_singleton  member\_append"  h\mcdot{}  THEN  Auto)  )\mcdot{})

---

Home Index