---

Step * 1 1 4 2 2 of Lemma bar26_4a_imp_fan26_6a


1. g: List  . R,A: List  .
     (spr(g)
      ((g []) = 0)
      (a: List. (((g a) = 0)  Dec(R a)))
      (f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f)))))
      (a: List. (((g a) = 0)  (R a)  (A a)))
      (a: List. (((g a) = 0)  (s:. (((g (a @ [s])) = 0)  (A (a @ [s]))))  (A a)))
      (A []))@i'
2. B :  List  @i
3. R :  List  @i'
4. a: List. Dec(R a)@i
5. f:fin_spr(B). x:. (R mklist(x;f))@i
6. a :  List@i
7. if (a  fspr(B)) then 0 else 1 fi  = 0@i
8. s:
     ((if (a @ [s]  fspr(B)) then 0 else 1 fi  = 0)
      (z:
          f:  
            ((t:. ((f t)  (B ((a @ [s]) @ mklist(t;f)))))  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))@i
9. (a  fspr(B))
10. s:
      ((s  (B a))
       (z:
           f:  
             ((t:. ((f t)  (B ((a @ [s]) @ mklist(t;f)))))  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))
11. b:
      ((s:
          ((s  b)
           (z:
               f:  
                 ((x:. ((f x)  (B ((a @ [s]) @ mklist(x;f)))))
                  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f)))))))))
       (z:
           s:
             ((s  b)
              (f:  
                   ((x:. ((f x)  (B ((a @ [s]) @ mklist(x;f)))))
                    (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))))
 z:. f:  . ((t:. ((f t)  (B (a @ mklist(t;f)))))  (x:. ((x  z)  (R (a @ mklist(x;f))))))
BY
{ (InstHyp [B a] (-1) THENA (Try (Trivial ) THEN Auto THEN skip{auto is only for wf goal. antecendent is hyp 10}))
 }

1
1. g: List  . R,A: List  .
     (spr(g)
      ((g []) = 0)
      (a: List. (((g a) = 0)  Dec(R a)))
      (f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f)))))
      (a: List. (((g a) = 0)  (R a)  (A a)))
      (a: List. (((g a) = 0)  (s:. (((g (a @ [s])) = 0)  (A (a @ [s]))))  (A a)))
      (A []))@i'
2. B :  List  @i
3. R :  List  @i'
4. a: List. Dec(R a)@i
5. f:fin_spr(B). x:. (R mklist(x;f))@i
6. a :  List@i
7. if (a  fspr(B)) then 0 else 1 fi  = 0@i
8. s:
     ((if (a @ [s]  fspr(B)) then 0 else 1 fi  = 0)
      (z:
          f:  
            ((t:. ((f t)  (B ((a @ [s]) @ mklist(t;f)))))  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))@i
9. (a  fspr(B))
10. s:
      ((s  (B a))
       (z:
           f:  
             ((t:. ((f t)  (B ((a @ [s]) @ mklist(t;f)))))  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))
11. b:
      ((s:
          ((s  b)
           (z:
               f:  
                 ((x:. ((f x)  (B ((a @ [s]) @ mklist(x;f)))))
                  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f)))))))))
       (z:
           s:
             ((s  b)
              (f:  
                   ((x:. ((f x)  (B ((a @ [s]) @ mklist(x;f)))))
                    (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))))
12. z:
     s:
       ((s  (B a))
        (f:  
             ((x:. ((f x)  (B ((a @ [s]) @ mklist(x;f)))))  (x:. ((x  z)  (R ((a @ [s]) @ mklist(x;f))))))))
 z:. f:  . ((t:. ((f t)  (B (a @ mklist(t;f)))))  (x:. ((x  z)  (R (a @ mklist(x;f))))))



1.  \mforall{}g:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}R,A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.
          (spr(g)
          {}\mRightarrow{}  ((g  [])  =  0)
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  Dec(R  a)))
          {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}x:\mBbbN{}.  ((g  mklist(x;f))  =  0))  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  (R  mklist(x;f)))))
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  (R  a)  {}\mRightarrow{}  (A  a)))
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  (\mforall{}s:\mBbbN{}.  (((g  (a  @  [s]))  =  0)  {}\mRightarrow{}  (A  (a  @  [s]))))  {}\mRightarrow{}  (A  a)))
          {}\mRightarrow{}  (A  []))@i'
2.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}a:\mBbbN{}  List.  Dec(R  a)@i
5.  \mforall{}f:fin\_spr(B).  \mexists{}x:\mBbbN{}.  (R  mklist(x;f))@i
6.  a  :  \mBbbN{}  List@i
7.  if  (a  \mmember{}  fspr(B))  then  0  else  1  fi    =  0@i
8.  \mforall{}s:\mBbbN{}
          ((if  (a  @  [s]  \mmember{}  fspr(B))  then  0  else  1  fi    =  0)
          {}\mRightarrow{}  (\mexists{}z:\mBbbN{}
                    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                        ((\mforall{}t:\mBbbN{}.  ((f  t)  \mleq{}  (B  ((a  @  [s])  @  mklist(t;f)))))
                        {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  ((a  @  [s])  @  mklist(x;f))))))))@i
9.  \muparrow{}(a  \mmember{}  fspr(B))
10.  \mforall{}s:\mBbbN{}
            ((s  \mleq{}  (B  a))
            {}\mRightarrow{}  (\mexists{}z:\mBbbN{}
                      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                          ((\mforall{}t:\mBbbN{}.  ((f  t)  \mleq{}  (B  ((a  @  [s])  @  mklist(t;f)))))
                          {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  ((a  @  [s])  @  mklist(x;f))))))))
11.  \mforall{}b:\mBbbN{}
            ((\mforall{}s:\mBbbN{}
                    ((s  \mleq{}  b)
                    {}\mRightarrow{}  (\mexists{}z:\mBbbN{}
                              \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                                  ((\mforall{}x:\mBbbN{}.  ((f  x)  \mleq{}  (B  ((a  @  [s])  @  mklist(x;f)))))
                                  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  ((a  @  [s])  @  mklist(x;f)))))))))
            {}\mRightarrow{}  (\mexists{}z:\mBbbN{}
                      \mforall{}s:\mBbbN{}
                          ((s  \mleq{}  b)
                          {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                                      ((\mforall{}x:\mBbbN{}.  ((f  x)  \mleq{}  (B  ((a  @  [s])  @  mklist(x;f)))))
                                      {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  ((a  @  [s])  @  mklist(x;f))))))))))
\mvdash{}  \mexists{}z:\mBbbN{}
      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}t:\mBbbN{}.  ((f  t)  \mleq{}  (B  (a  @  mklist(t;f)))))  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  (a  @  mklist(x;f))))))


By

(InstHyp  [\mkleeneopen{}B  a\mkleeneclose{}]  (-1)\mcdot{}
  THENA  (Try  (Trivial  \mcdot{})  THEN  Auto  THEN  skip\{auto  is  only  for  wf  goal.  antecendent  is  hyp  10\})
  )\mcdot{}



Home Index