Step
*
2
1
1
1
of Lemma
permutation-invariant2
1. [T] : Type
2. [R] : (T List) ⟶ (T List) ⟶ ℙ
3. Trans(T List;x,y.R[x;y])
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)]
13. u : T
14. u1 : T
15. v : T List
⊢ R[[u; [u1 / v]];([u; [u1 / v]] o (0, 1))]
BY
{ (Subst ⌜([u; [u1 / v]] o (0, 1)) = [u1; [u / v]] ∈ (T List)⌝ 0⋅ THEN Auto) }
1
.....equality.....
1. T : Type
2. R : (T List) ⟶ (T List) ⟶ ℙ
3. Trans(T List;x,y.R[x;y])
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)]
13. u : T
14. u1 : T
15. v : T List
⊢ ([u; [u1 / v]] o (0, 1)) = [u1; [u / v]] ∈ (T List)
Latex:
Latex:
1. [T] : Type
2. [R] : (T List) {}\mrightarrow{} (T List) {}\mrightarrow{} \mBbbP{}
3. Trans(T List;x,y.R[x;y])
4. Refl(T List;as,bs.R[as;bs])
5. \mforall{}as:T List. \mforall{}a:T. R[[a / as];as @ [a]]
6. \mforall{}as:T List. \mforall{}a1,a2:T. R[[a1; [a2 / as]];[a2; [a1 / as]]]
7. as : T List
8. f : \mBbbN{}||as|| {}\mrightarrow{} \mBbbN{}||as||
9. Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
10. 1 < ||as||
11. f1 : \{f:\mBbbN{}||as|| {}\mrightarrow{} \mBbbN{}||as||| Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)\}
12. R[as;(as o f1)]
13. u : T
14. u1 : T
15. v : T List
\mvdash{} R[[u; [u1 / v]];([u; [u1 / v]] o (0, 1))]
By
Latex:
(Subst \mkleeneopen{}([u; [u1 / v]] o (0, 1)) = [u1; [u / v]]\mkleeneclose{} 0\mcdot{} THEN Auto)
Home
Index