---

Step * 2 1 1 1 1 of Lemma least-equiv-is-equiv-1


1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. a : A
4. b : A
5. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
6. rel_path(A;L;a;b) ∧ 0 < ||L||
⊢ rev(map(λt.let a,b,r = t in 
             <b, a, case r of inl(x) => inr x  | inr(x) => inl x>;L)) ∈ {L:(a:A × b:A × ((R a b) ∨ (R b a))) List| 
                                                                         rel_path(A;L;b;a) ∧ 0 < ||L||} 
BY
{ MemTypeCD }

1
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. a : A
4. b : A
5. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
6. rel_path(A;L;a;b) ∧ 0 < ||L||
⊢ rev(map(λt.let a,b,r = t in 
             <b, a, case r of inl(x) => inr x  | inr(x) => inl x>;L)) ∈ (a:A × b:A × ((R a b) ∨ (R b a))) List

2
.....set predicate..... 
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. a : A
4. b : A
5. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
6. rel_path(A;L;a;b) ∧ 0 < ||L||
⊢ rel_path(A;rev(map(λt.let a,b,r = t in 
                        <b, a, case r of inl(x) => inr x  | inr(x) => inl x>;L));b;a)
∧ 0 < ||rev(map(λt.let a,b,r = t in 
                   <b, a, case r of inl(x) => inr x  | inr(x) => inl x>;L))||

3
.....wf..... 
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. a : A
4. b : A
5. L : (a:A × b:A × ((R a b) ∨ (R b a))) List
6. rel_path(A;L;a;b) ∧ 0 < ||L||
7. L1 : (a:A × b:A × ((R a b) ∨ (R b a))) List
⊢ istype(rel_path(A;L1;b;a) ∧ 0 < ||L1||)

---

Latex:

---

Latex:

1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  a  :  A
4.  b  :  A
5.  L  :  (a:A  \mtimes{}  b:A  \mtimes{}  ((R  a  b)  \mvee{}  (R  b  a)))  List
6.  rel\_path(A;L;a;b)  \mwedge{}  0  <  ||L||
\mvdash{}  rev(map(\mlambda{}t.let  a,b,r  =  t  in 
                          <b,  a,  case  r  of  inl(x)  =>  inr  x    |  inr(x)  =>  inl  x>L))  \mmember{}  \{L:(a:A
                                                                                                                                                  \mtimes{}  b:A
                                                                                                                                                  \mtimes{}  ((R  a  b)
                                                                                                                                                      \mvee{}  (R  b  a)))  List| 
                                                                                                                                                  rel\_path(A;L;b;a)
                                                                                                                                                  \mwedge{}  0  <  ||L||\} 


By

---

Latex:
MemTypeCD

---

Home Index