Step * of Lemma mk_applies_lambdas

No Annotations
[F,G:Top]. ∀[m:ℕ]. ∀[n:ℕ1].  (mk_applies(mk_lambdas(F;m);G;n) mk_lambdas(F;m n))
BY
(Auto
   THEN SqEqualTopToBase
   THEN (Assert n ≤ BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜N ∈ ℕ⌝⋅ THENA Auto)
   THEN ThinVar `n'
   THEN RenameVar `n' (-1)
   THEN NatInd (-1)
   THEN Try (Complete ((RepUR ``mk_applies`` THEN Subst ⌜m⌝ 0⋅ THEN Auto)))
   THEN (ParallelLast THENA Auto)) }

1
1. : ℕ
2. Base
3. Base
4. : ℤ
5. 0 < n
6. n ≤ m
7. mk_applies(mk_lambdas(F;m);G;n 1) mk_lambdas(F;m 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