Step * of Lemma permutation-generators4

n:ℕ
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
    (P[λx.x]
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n.  (P[f]  P[f (0, j)]))
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))
BY
(InstLemma `permutation-generators3` []
   THEN RepeatFor (ParallelLast')
   THEN Auto
   THEN Try ((BLemma `compose-injections` THEN Auto))
   THEN BHyp -1 
   THEN Auto) }

1
1. : ℕ
2. [P] {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n.  (P[f]  P[f (0, j)])
5. {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f]  P[f (i, j)] supposing i < j)
 (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f])
7. f1 {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
8. : ℕn
9. : ℕn
10. i < j
11. P[f1]
⊢ P[f1 (i, j)]


Latex:


Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[P:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}]
        (P[\mlambda{}x.x]
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}j:\mBbbN{}\msupplus{}n.    (P[f]  {}\mRightarrow{}  P[f  o  (0,  j)]))
        {}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f]))


By


Latex:
(InstLemma  `permutation-generators3`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  Try  ((BLemma  `compose-injections`  THEN  Auto))
  THEN  BHyp  -1 
  THEN  Auto)




Home Index