---

Step * of Lemma stamps-example-ext

∀n:ℕ. ∃i:ℕ. (∃j:ℕ [((n + 8) = ((3 * i) + (5 * j)) ∈ ℤ)])
BY
{ TACTIC:Extract of Obid: stamps-example
         not unfolding  primrec
         finishing with Auto
         normalizes to:
         
         λn.primrec(n;<1, 1>;λi,x. let i,j = x 
                                 in if (i) < (3)
                                       then eval i' = i + 2 in
                                            eval j' = j - 1 in
                                              <i', j'>
                                       else eval i' = i - 3 in
                                            eval j' = j + 2 in
                                              <i', j'>) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((n  +  8)  =  ((3  *  i)  +  (5  *  j)))])


By

---

Latex:
TACTIC:Extract  of  Obid:  stamps-example
              not  unfolding    primrec
              finishing  with  Auto
              normalizes  to:
             
              \mlambda{}n.primrec(n;ə,  1>\mlambda{}i,x.  let  i,j  =  x 
                                                              in  if  (i)  <  (3)
                                                                          then  eval  i'  =  i  +  2  in
                                                                                    eval  j'  =  j  -  1  in
                                                                                        <i',  j'>
                                                                          else  eval  i'  =  i  -  3  in
                                                                                    eval  j'  =  j  +  2  in
                                                                                        <i',  j'>)

---

Home Index