Step * of Lemma flip-generators

n:ℕ
  ∀i,j:ℕn.  ∃L:𝔹 List. ((i, j) reduce(λi,g. (if then rot(n) else (0, 1) fi  g);λx.x;L) ∈ (ℕn ⟶ ℕn)) supposing 1 <\000C n
BY
TACTIC:(InstLemma `flip-adjacent` []
          THEN ParallelLast'
          THEN (D THENA Auto)
          THEN PromoteHyp (-1) 2
          THEN RepeatFor (ParallelLast')
          THEN ExRepD) }

1
1. : ℕ
2. 1 < n
3. : ℕn
4. : ℕn
5. : ℕList
6. (i, j) reduce(λi,g. ((i, 1) g);λx.x;L) ∈ (ℕn ⟶ ℕn)
⊢ ∃L:𝔹 List. ((i, j) reduce(λi,g. (if then rot(n) else (0, 1) fi  g);λx.x;L) ∈ (ℕn ⟶ ℕn))


Latex:


Latex:
\mforall{}n:\mBbbN{}
    \mforall{}i,j:\mBbbN{}n.    \mexists{}L:\mBbbB{}  List.  ((i,  j)  =  reduce(\mlambda{}i,g.  (if  i  then  rot(n)  else  (0,  1)  fi    o  g);\mlambda{}x.x;L)) 
    supposing  1  <  n


By


Latex:
TACTIC:(InstLemma  `flip-adjacent`  []
                THEN  ParallelLast'
                THEN  (D  0  THENA  Auto)
                THEN  PromoteHyp  (-1)  2
                THEN  RepeatFor  2  (ParallelLast')
                THEN  ExRepD)




Home Index