Step
*
of Lemma
mk_applies_lambdas
No Annotations
∀[F,G:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].  (mk_applies(mk_lambdas(F;m);G;n) ~ mk_lambdas(F;m - n))
BY
{ (Auto
   THEN SqEqualTopToBase
   THEN (Assert n ≤ m BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜n = N ∈ ℕ⌝⋅ THENA Auto)
   THEN ThinVar `n'
   THEN RenameVar `n' (-1)
   THEN NatInd (-1)
   THEN Try (Complete ((RepUR ``mk_applies`` 0 THEN Subst ⌜m - 0 ~ m⌝ 0⋅ THEN Auto)))
   THEN (ParallelLast THENA Auto)) }
1
1. m : ℕ
2. G : Base
3. F : Base
4. n : ℤ
5. 0 < n
6. n ≤ m
7. mk_applies(mk_lambdas(F;m);G;n - 1) ~ mk_lambdas(F;m - n - 1)
⊢ mk_applies(mk_lambdas(F;m);G;n) ~ mk_lambdas(F;m - n)
Latex:
Latex:
No  Annotations
\mforall{}[F,G:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].    (mk\_applies(mk\_lambdas(F;m);G;n)  \msim{}  mk\_lambdas(F;m  -  n))
By
Latex:
(Auto
  THEN  SqEqualTopToBase
  THEN  (Assert  n  \mleq{}  m  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}n  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `n'
  THEN  RenameVar  `n'  (-1)
  THEN  NatInd  (-1)
  THEN  Try  (Complete  ((RepUR  ``mk\_applies``  0  THEN  Subst  \mkleeneopen{}m  -  0  \msim{}  m\mkleeneclose{}  0\mcdot{}  THEN  Auto)))
  THEN  (ParallelLast  THENA  Auto))
Home
Index