---

Step * of Lemma mutual-primitive-recursion

∀[A,B:Type].
  ∀f0:A. ∀g0:B. ∀F:ℕ ⟶ A ⟶ B ⟶ A. ∀G:ℕ ⟶ A ⟶ B ⟶ B.
    ∃f:ℕ ⟶ A
     ∃g:ℕ ⟶ B
      (((f 0) = f0 ∈ A)
      ∧ ((g 0) = g0 ∈ B)
      ∧ (∀s:ℕ+. (((f s) = F[s - 1;f (s - 1);g (s - 1)] ∈ A) ∧ ((g s) = G[s - 1;f (s - 1);g (s - 1)] ∈ B))))
BY
{ (Auto
   THEN (InstConcl [⌜λs.(fst(primrec(s;<f0, g0>;λs,p. let x,y = p in <F[s;x;y], G[s;x;y]>)))⌝; 
   ⌜λs.(snd(primrec(s;<f0, g0>;λs,p. let x,y = p in <F[s;x;y], G[s;x;y]>)))⌝])⋅
   THEN Reduce 0
   THEN Repeat ((MemCD THEN Try (Complete (Auto))))
   THEN Auto
   THEN ((RW (AddrC [2;1] (LemmaC `primrec-unroll`)) 0) THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN (GenConclAtAddr [2; 1; 1])
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}f0:A.  \mforall{}g0:B.  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  A.  \mforall{}G:\mBbbN{}  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.
        \mexists{}f:\mBbbN{}  {}\mrightarrow{}  A
          \mexists{}g:\mBbbN{}  {}\mrightarrow{}  B
            (((f  0)  =  f0)
            \mwedge{}  ((g  0)  =  g0)
            \mwedge{}  (\mforall{}s:\mBbbN{}\msupplus{}.  (((f  s)  =  F[s  -  1;f  (s  -  1);g  (s  -  1)])  \mwedge{}  ((g  s)  =  G[s  -  1;f  (s  -  1);g  (s  -  1)]))))


By

---

Latex:
(Auto
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}s.(fst(primrec(s;<f0,  g0>\mlambda{}s,p.  let  x,y  =  p  in  <F[s;x;y],  G[s;x;y]>)))\mkleeneclose{}; 
  \mkleeneopen{}\mlambda{}s.(snd(primrec(s;<f0,  g0>\mlambda{}s,p.  let  x,y  =  p  in  <F[s;x;y],  G[s;x;y]>)))\mkleeneclose{}])\mcdot{}
  THEN  Reduce  0
  THEN  Repeat  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  Auto
  THEN  ((RW  (AddrC  [2;1]  (LemmaC  `primrec-unroll`))  0)  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  (GenConclAtAddr  [2;  1;  1])
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index