---

Step * of Lemma AF-uniform-induction

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[Q:T ⟶ ℙ]. uniform-TI(T;x,y.¬R[x;y];t.Q[t])) supposing 
     (AFx,y:T.R[x;y] and 
     (∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))))
BY
{ (Auto
   THEN UnfoldTopAb 0
   THEN UseWitness ⌜λF.fix(F)⌝⋅
   THEN (MemCD THENA Auto)
   THEN Unfold `uall` 0
   THEN (MemTypeCD THENA Auto)
   THEN (Assert ⌜(λn,s. if (n =z 0) then fix(F) else case s (n - 1) of inl(z) => fix(F) | inr(z) => Ax fi ) 0 ⊥
                 ∈ (λn,s. if (n =z 0) then Q[t] else case s (n - 1) of inl(z) => Q[z] | inr(z) => True fi ) 0 ⊥⌝⋅
   THENM (RepUR ``eq_int`` -1 THEN Trivial)
   )
   THEN (InstLemma `AF-spread-law_wf` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
   THEN (InstLemma `AFbar_wf` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
   THEN (Strong_Bar_Induction ⌜T?⌝ ⌜AF-spread-law(x,y.R[x;y])⌝ ⌜AFbar()⌝⋅ THENA Auto)
   THEN Try ((InstLemma `AF-path-barred` [⌜T⌝;⌜R⌝] ⋅ THEN Complete (Auto)))
   THEN Try ((Fold `decidable` 0 THEN InstLemma `decidable__AFbar` [⌜T⌝;⌜R⌝]⋅ THEN Auto))
   THEN All Reduce) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))
4. AFx,y:T.R[x;y]
5. Q : T ⟶ ℙ
6. F : ∀[t:T]. ((∀[s:{s:T| ¬R[t;s]} ]. Q[s]) ⇒ Q[t])
7. t : T
8. AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
9. AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ
10. n : ℕ
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. (AF-spread-law(x,y.R[x;y]) %9 s (s %9))
13. m : AFbar() n s
⊢ if (n =z 0) then fix(F) else case s (n - 1) of inl(z) => fix(F) | inr(z) => Ax fi  ∈ if (n =z 0)
  then Q[t]
  else case s (n - 1) of inl(z) => Q[z] | inr(z) => True
  fi 

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))
4. AFx,y:T.R[x;y]
5. Q : T ⟶ ℙ
6. F : ∀[t:T]. ((∀[s:{s:T| ¬R[t;s]} ]. Q[s]) ⇒ Q[t])
7. t : T
8. AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
9. AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ
10. n : ℕ
11. s : ℕn ⟶ (T?)
12. ∀%9:ℕn. (AF-spread-law(x,y.R[x;y]) %9 s (s %9))
13. ∀t1:{t1:T?| AF-spread-law(x,y.R[x;y]) n s t1} 
      (if (n + 1 =z 0)
       then fix(F)
       else case if (n + 1) - 1=n  then t1  else (s ((n + 1) - 1)) of inl(z) => fix(F) | inr(z) => Ax
       fi  ∈ if (n + 1 =z 0)
       then Q[t]
       else case if (n + 1) - 1=n  then t1  else (s ((n + 1) - 1)) of inl(z) => Q[z] | inr(z) => True
       fi )
⊢ if (n =z 0) then fix(F) else case s (n - 1) of inl(z) => fix(F) | inr(z) => Ax fi  ∈ if (n =z 0)
  then Q[t]
  else case s (n - 1) of inl(z) => Q[z] | inr(z) => True
  fi 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  uniform-TI(T;x,y.\mneg{}R[x;y];t.Q[t]))  supposing 
          (AFx,y:T.R[x;y]  and 
          (\mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  0
  THEN  UseWitness  \mkleeneopen{}\mlambda{}F.fix(F)\mkleeneclose{}\mcdot{}
  THEN  (MemCD  THENA  Auto)
  THEN  Unfold  `uall`  0
  THEN  (MemTypeCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\mlambda{}n,s.  if  (n  =\msubz{}  0)
                                          then  fix(F)
                                          else  case  s  (n  -  1)  of  inl(z)  =>  fix(F)  |  inr(z)  =>  Ax
                                          fi  ) 
                              0 
                              \mbot{}  \mmember{}  (\mlambda{}n,s.  if  (n  =\msubz{}  0)
                                                  then  Q[t]
                                                  else  case  s  (n  -  1)  of  inl(z)  =>  Q[z]  |  inr(z)  =>  True
                                                  fi  ) 
                                      0 
                                      \mbot{}\mkleeneclose{}\mcdot{}
  THENM  (RepUR  ``eq\_int``  -1  THEN  Trivial)
  )
  THEN  (InstLemma  `AF-spread-law\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `AFbar\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Strong\_Bar\_Induction  \mkleeneopen{}T?\mkleeneclose{}  \mkleeneopen{}AF-spread-law(x,y.R[x;y])\mkleeneclose{}  \mkleeneopen{}AFbar()\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((InstLemma  `AF-path-barred`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]  \mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  ((Fold  `decidable`  0  THEN  InstLemma  `decidable\_\_AFbar`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  All  Reduce)

---

Home Index