Step * 2 4 of Lemma fun-path-cons


1. Type
2. T ⟶ T
3. T
4. List
5. T
6. T
7. T
8. y ∈ T
9. ((y (f u) ∈ T) ∧ (y u ∈ T)))
   ∧ 0 < ||v|| 1
   ∧ (u u ∈ T)
   ∧ (x [u v][(||v|| 1) 1] ∈ T)
   ∧ (∀i:ℕ(||v|| 1) 1. (([u v][i] (f [u v][i 1]) ∈ T) ∧ ([u v][i] [u v][i 1] ∈ T)))) 
   supposing 0 < ||v|| 1
10. y ∈ supposing ¬0 < ||v|| 1
11. : ℕ((||v|| 1) 1) 1
⊢ ¬([y; [u v]][i] [y; [u v]][i 1] ∈ T)
BY
((D (-3) THEN Auto')⋅
   THEN CaseNat `i'
   THEN (Reduce THEN Auto)
   THEN RWO "select_cons_tl" (0)
   THEN Auto'
   THEN InstHyp [⌜1⌝(-2)⋅
   THEN Auto')⋅ }


Latex:


Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  v  :  T  List
5.  x  :  T
6.  y  :  T
7.  z  :  T
8.  z  =  y
9.  ((y  =  (f  u))  \mwedge{}  (\mneg{}(y  =  u)))
      \mwedge{}  0  <  ||v||  +  1
      \mwedge{}  (u  =  u)
      \mwedge{}  (x  =  [u  /  v][(||v||  +  1)  -  1])
      \mwedge{}  (\mforall{}i:\mBbbN{}(||v||  +  1)  -  1.  (([u  /  v][i]  =  (f  [u  /  v][i  +  1]))  \mwedge{}  (\mneg{}([u  /  v][i]  =  [u  /  v][i  +  1])))) 
      supposing  0  <  ||v||  +  1
10.  x  =  y  supposing  \mneg{}0  <  ||v||  +  1
11.  i  :  \mBbbN{}((||v||  +  1)  +  1)  -  1
\mvdash{}  \mneg{}([y;  [u  /  v]][i]  =  [y;  [u  /  v]][i  +  1])


By


Latex:
((D  (-3)  THEN  Auto')\mcdot{}
  THEN  CaseNat  0  `i'
  THEN  (Reduce  0  THEN  Auto)
  THEN  RWO  "select\_cons\_tl"  (0)
  THEN  Auto'
  THEN  InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto')\mcdot{}




Home Index