Step * 1 1 of Lemma pcw-partial_wf

.....set predicate..... 
1. Type
2. P ⟶ Type
3. p:P ⟶ A[p] ⟶ Type
4. p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
6. ∀i:ℕStepRel(path i;path (i 1))
7. : ℕ
⊢ let n,ss = <n, path> 
  in ∀i:ℕ1. StepRel(ss i;ss (i 1))
BY
(Reduce THEN Auto) }


Latex:


Latex:
.....set  predicate..... 
1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  path  :  \mBbbN{}  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
6.  \mforall{}i:\mBbbN{}.  StepRel(path  i;path  (i  +  1))
7.  n  :  \mBbbN{}
\mvdash{}  let  n,ss  =  <n,  path> 
    in  \mforall{}i:\mBbbN{}n  -  1.  StepRel(ss  i;ss  (i  +  1))


By


Latex:
(Reduce  0  THEN  Auto)




Home Index