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


1. Top
2. Top
3. : ℕ+
⊢ 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 THENA Auto)
      THEN Reduce 0
      THEN Try (Complete (Auto))
      THEN (Subst' (m 1) THENA Auto)
      THEN (RWO "primrec-unroll" THENA Auto)
      THEN (SplitOnConclITE THENA Auto)
      THEN Reduce 0
      THEN Try ((HypSubst' -2 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