---

Step * 2 1 1 1 2 1 1 of Lemma bar-separation-implies-twkl!

.....assertion..... 
1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. ∀a,b:T.  Dec(a = b ∈ T)
10. eff-unique-path(T;A)
11. ∀s:T List. ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
12. g : s:(T List) ⟶ T
13. ∀s:T List. ∀t':T.  ((¬(t' = (g s) ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
⊢ ∀n:ℕ
    ((||primrec(n;[];λn',s. (s @ [g s]))|| = n ∈ ℤ)
    ∧ (0 < n ⇒ (primrec(n;[];λn',s. (s @ [g s]))[n - 1] = (g primrec(n - 1;[];λn',s. (s @ [g s]))) ∈ T))
    ∧ (map(λn.primrec(n + 1;[];λn',s. (s @ [g s]))[n];upto(n)) = primrec(n;[];λn',s. (s @ [g s])) ∈ (T List)))
BY
{ (InductionOnNat THEN Reduce 0 THEN BetterSplitAndConcl THEN Auto)⋅ }

1
1. T : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. ∀a,b:T.  Dec(a = b ∈ T)
10. eff-unique-path(T;A)
11. ∀s:T List. ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
12. g : s:(T List) ⟶ T
13. ∀s:T List. ∀t':T.  ((¬(t' = (g s) ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
14. n : ℤ
15. 0 < n
16. ||primrec(n - 1;[];λn',s. (s @ [g s]))|| = (n - 1) ∈ ℤ
17. 0 < n - 1 ⇒ (primrec(n - 1;[];λn',s. (s @ [g s]))[n - 1 - 1] = (g primrec(n - 1 - 1;[];λn',s. (s @ [g s]))) ∈ T)
18. map(λn.primrec(n + 1;[];λn',s. (s @ [g s]))[n];upto(n - 1)) = primrec(n - 1;[];λn',s. (s @ [g s])) ∈ (T List)
⊢ ||primrec(n;[];λn',s. (s @ [g s]))|| = n ∈ ℤ

2
1. T : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. ∀a,b:T.  Dec(a = b ∈ T)
10. eff-unique-path(T;A)
11. ∀s:T List. ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
12. g : s:(T List) ⟶ T
13. ∀s:T List. ∀t':T.  ((¬(t' = (g s) ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
14. n : ℤ
15. 0 < n
16. ||primrec(n - 1;[];λn',s. (s @ [g s]))|| = (n - 1) ∈ ℤ
17. 0 < n - 1 ⇒ (primrec(n - 1;[];λn',s. (s @ [g s]))[n - 1 - 1] = (g primrec(n - 1 - 1;[];λn',s. (s @ [g s]))) ∈ T)
18. map(λn.primrec(n + 1;[];λn',s. (s @ [g s]))[n];upto(n - 1)) = primrec(n - 1;[];λn',s. (s @ [g s])) ∈ (T List)
19. ||primrec(n;[];λn',s. (s @ [g s]))|| = n ∈ ℤ
20. 0 < n
⊢ primrec(n;[];λn',s. (s @ [g s]))[n - 1] = (g primrec(n - 1;[];λn',s. (s @ [g s]))) ∈ T

3
1. T : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. ∀a,b:T.  Dec(a = b ∈ T)
10. eff-unique-path(T;A)
11. ∀s:T List. ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
12. g : s:(T List) ⟶ T
13. ∀s:T List. ∀t':T.  ((¬(t' = (g s) ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
14. n : ℤ
15. 0 < n
16. ||primrec(n - 1;[];λn',s. (s @ [g s]))|| = (n - 1) ∈ ℤ
17. 0 < n - 1 ⇒ (primrec(n - 1;[];λn',s. (s @ [g s]))[n - 1 - 1] = (g primrec(n - 1 - 1;[];λn',s. (s @ [g s]))) ∈ T)
18. map(λn.primrec(n + 1;[];λn',s. (s @ [g s]))[n];upto(n - 1)) = primrec(n - 1;[];λn',s. (s @ [g s])) ∈ (T List)
19. ||primrec(n;[];λn',s. (s @ [g s]))|| = n ∈ ℤ
20. primrec(n;[];λn',s. (s @ [g s]))[n - 1] = (g primrec(n - 1;[];λn',s. (s @ [g s]))) ∈ T
⊢ map(λn.primrec(n + 1;[];λn',s. (s @ [g s]))[n];upto(n)) = primrec(n;[];λn',s. (s @ [g s])) ∈ (T List)

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  \mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size
3.  BarSep(T;T)
4.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
5.  \mneg{}tbar(T;\mneg{}(A))
6.  Decidable(A)
7.  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (A  bs)  {}\mRightarrow{}  (A  as))
8.  T
9.  \mforall{}a,b:T.    Dec(a  =  b)
10.  eff-unique-path(T;A)
11.  \mforall{}s:T  List.  \mexists{}t:T.  \mforall{}t':T.  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))
12.  g  :  s:(T  List)  {}\mrightarrow{}  T
13.  \mforall{}s:T  List.  \mforall{}t':T.    ((\mneg{}(t'  =  (g  s)))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))
\mvdash{}  \mforall{}n:\mBbbN{}
        ((||primrec(n;[];\mlambda{}n',s.  (s  @  [g  s]))||  =  n)
        \mwedge{}  (0  <  n  {}\mRightarrow{}  (primrec(n;[];\mlambda{}n',s.  (s  @  [g  s]))[n  -  1]  =  (g  primrec(n  -  1;[];\mlambda{}n',s.  (s  @  [g  s]))))\000C)
        \mwedge{}  (map(\mlambda{}n.primrec(n  +  1;[];\mlambda{}n',s.  (s  @  [g  s]))[n];upto(n))  =  primrec(n;[];\mlambda{}n',s.  (s  @  [g  s]))))


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  BetterSplitAndConcl  THEN  Auto)\mcdot{}

---

Home Index