---

Step * of Lemma permutation-invariant2

No Annotations
∀[T:Type]. ∀[R:(T List) ⟶ (T List) ⟶ ℙ].
  (Trans(T List;as,bs.R[as;bs])
  ⇒ Refl(T List;as,bs.R[as;bs])
  ⇒ (∀as:T List. ∀a:T.  R[[a / as];as @ [a]])
  ⇒ (∀as:T List. ∀a1,a2:T.  R[[a1; [a2 / as]];[a2; [a1 / as]]])
  ⇒ (∀as,bs:T List.  (permutation(T;as;bs) ⇒ R[as;bs])))
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN (HypSubst' -1 0 THEN Auto)
   THEN ThinVar `bs'
   THEN InstLemma `permutation-generators2` [⌜||as||⌝;⌜λ2f.R[as;(as o f)]⌝]⋅
   THEN Auto') }

1
.....antecedent..... 
1. [T] : Type
2. [R] : (T List) ⟶ (T List) ⟶ ℙ
3. Trans(T List;as,bs.R[as;bs])
4. Refl(T List;as,bs.R[as;bs])
5. ∀as:T List. ∀a:T.  R[[a / as];as @ [a]]
6. ∀as:T List. ∀a1,a2:T.  R[[a1; [a2 / as]];[a2; [a1 / as]]]
7. as : T List
8. f : ℕ||as|| ⟶ ℕ||as||
9. Inj(ℕ||as||;ℕ||as||;f)
⊢ R[as;(as o λx.x)]

2
1. [T] : Type
2. [R] : (T List) ⟶ (T List) ⟶ ℙ
3. Trans(T List;as,bs.R[as;bs])
4. Refl(T List;as,bs.R[as;bs])
5. ∀as:T List. ∀a:T.  R[[a / as];as @ [a]]
6. ∀as:T List. ∀a1,a2:T.  R[[a1; [a2 / as]];[a2; [a1 / as]]]
7. as : T List
8. f : ℕ||as|| ⟶ ℕ||as||
9. Inj(ℕ||as||;ℕ||as||;f)
10. 1 < ||as||
11. f1 : {f:ℕ||as|| ⟶ ℕ||as||| Inj(ℕ||as||;ℕ||as||;f)} 
12. R[as;(as o f1)]
⊢ R[as;(as o f1 o (0, 1))]

3
1. [T] : Type
2. [R] : (T List) ⟶ (T List) ⟶ ℙ
3. Trans(T List;as,bs.R[as;bs])
4. Refl(T List;as,bs.R[as;bs])
5. ∀as:T List. ∀a:T.  R[[a / as];as @ [a]]
6. ∀as:T List. ∀a1,a2:T.  R[[a1; [a2 / as]];[a2; [a1 / as]]]
7. as : T List
8. f : ℕ||as|| ⟶ ℕ||as||
9. Inj(ℕ||as||;ℕ||as||;f)
10. f1 : {f:ℕ||as|| ⟶ ℕ||as||| Inj(ℕ||as||;ℕ||as||;f)} 
11. R[as;(as o f1)]
⊢ R[as;(as o f1 o rot(||as||))]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[R:(T  List)  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T  List;as,bs.R[as;bs])
    {}\mRightarrow{}  Refl(T  List;as,bs.R[as;bs])
    {}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a:T.    R[[a  /  as];as  @  [a]])
    {}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a1,a2:T.    R[[a1;  [a2  /  as]];[a2;  [a1  /  as]]])
    {}\mRightarrow{}  (\mforall{}as,bs:T  List.    (permutation(T;as;bs)  {}\mRightarrow{}  R[as;bs])))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  (HypSubst'  -1  0  THEN  Auto)
  THEN  ThinVar  `bs'
  THEN  InstLemma  `permutation-generators2`  [\mkleeneopen{}||as||\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.R[as;(as  o  f)]\mkleeneclose{}]\mcdot{}
  THEN  Auto')

---

Home Index