---

Step * 2 2 1 1 1 1 1 of Lemma uncurry_wf


1. x : Top
2. y : Top
3. m : ℕ+
⊢ primrec(m - 1;y;λi,z. (z (x i))) (x (m - 1)) ~ primrec(m - 1;y (x 0);λi,z. (z (x (i + 1))))
BY
{ xxx(SqEqualTopToBase
      THEN (NatPlusInd 1 THENA Auto)
      THEN Reduce 0
      THEN Try (Complete (Auto))
      THEN (Subst' (m + 1) - 1 ~ m 0 THENA Auto)
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN (SplitOnConclITE THENA Auto)
      THEN Reduce 0
      THEN Try ((HypSubst' -2 0 THEN EqCD))
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  x  :  Top
2.  y  :  Top
3.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  primrec(m  -  1;y;\mlambda{}i,z.  (z  (x  i)))  (x  (m  -  1))  \msim{}  primrec(m  -  1;y  (x  0);\mlambda{}i,z.  (z  (x  (i  +  1))))


By

---

Latex:
xxx(SqEqualTopToBase
        THEN  (NatPlusInd  1  THENA  Auto)
        THEN  Reduce  0
        THEN  Try  (Complete  (Auto))
        THEN  (Subst'  (m  +  1)  -  1  \msim{}  m  0  THENA  Auto)
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  (SplitOnConclITE  THENA  Auto)
        THEN  Reduce  0
        THEN  Try  ((HypSubst'  -2  0  THEN  EqCD))
        THEN  Auto)xxx

---

Home Index