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