Step * 2 of Lemma tuple-equiv-is-equiv


1. (X:Type × (X ⟶ X ⟶ ℙ)) List
2. ∀i:ℕ||L||. let X,E L[i] in EquivRel(X;x,y.E y)
3. tuple-type(map(λp.(fst(p));L))
4. tuple-type(map(λp.(fst(p));L))
5. ∀i:ℕ||L||. ((snd(L[i])) a.i b.i)
⊢ ∀i:ℕ||L||. ((snd(L[i])) b.i a.i)
BY
(ParallelLast
   THEN MoveToConcl (-1)
   THEN (D With ⌜i⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN -2
   THEN Reduce 0) }

1
1. (X:Type × (X ⟶ X ⟶ ℙ)) List
2. tuple-type(map(λp.(fst(p));L))
3. tuple-type(map(λp.(fst(p));L))
4. ∀i:ℕ||L||. ((snd(L[i])) a.i b.i)
5. : ℕ||L||
6. Type
7. v1 X ⟶ X ⟶ ℙ
8. L[i] = <X, v1> ∈ (X:Type × (X ⟶ X ⟶ ℙ))
⊢ EquivRel(X;x,y.v1 y)  (v1 a.i b.i)  (v1 b.i a.i)


Latex:


Latex:

1.  L  :  (X:Type  \mtimes{}  (X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}))  List
2.  \mforall{}i:\mBbbN{}||L||.  let  X,E  =  L[i]  in  EquivRel(X;x,y.E  x  y)
3.  a  :  tuple-type(map(\mlambda{}p.(fst(p));L))
4.  b  :  tuple-type(map(\mlambda{}p.(fst(p));L))
5.  \mforall{}i:\mBbbN{}||L||.  ((snd(L[i]))  a.i  b.i)
\mvdash{}  \mforall{}i:\mBbbN{}||L||.  ((snd(L[i]))  b.i  a.i)


By


Latex:
(ParallelLast
  THEN  MoveToConcl  (-1)
  THEN  (D  2  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  D  -2
  THEN  Reduce  0)




Home Index