---

Step * of Lemma simple-cbva-seq-list

∀F:Top. ∀L1,L2:ℤ ⟶ Base. ∀m:ℕ.  ((∀j:ℕm + 1. (L1 j ~ L2 j)) ⇒ (simple-cbva-seq(L1;F;m) ~ simple-cbva-seq(L2;F;m)))
BY
{ (RepeatFor 5 (TACTIC:(D 0 THENA Auto))
   THEN RepUR ``simple-cbva-seq cbva-seq`` 0
   THEN AutoSplit
   THEN Try (HypSubst' (-1) 0)
   THEN Try (Complete ((RecUnfold `callbyvalueall-seq` 0 THEN AutoSplit)))
   THEN (GenConclAtAddrType ⌜ℕ⌝ [1;4]⋅ THENA Auto)
   THEN (Assert ⌜v ≤ m⌝⋅ THENA Auto)
   THEN RenameVar `n' (-3)
   THEN Thin (-2)
   THEN (GenConclAtAddrType ⌜Top⌝ [1;2]⋅ THENA Auto)
   THEN RenameVar `K' (-2)
   THEN Thin (-1)
   THEN ((GenConclAtAddrType ⌜Top⌝ [1;3]⋅ THENA Auto)
         THEN RenameVar `G' (-2)
         THEN Thin (-1)
         THEN (Assert ⌜∃k:ℕ. (m = (n + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
         THEN D (-1)
         THEN MoveToConcl (-7)
         THEN HypSubst' (-1) 0
         THEN ThinVar `m'
         THEN RepeatFor 2 (MoveToConcl (-3))
         THEN NatInd (-1)
         THEN ((UnivCD THENA Auto)
               THEN (RecUnfold `callbyvalueall-seq` 0
                     THEN AutoSplit
                     THEN MemCD
                     THEN Try (Complete ((RWO "-1" 0 THEN Auto)))
                     THEN (InstHyp [⌜n + 1⌝;⌜λf.(K f v)⌝] (-6)⋅
                           THENA (Try (Complete (Auto)) THEN Subst ⌜(n + 1) + (k - 1) ~ n + k⌝ 0⋅ THEN Auto)
                           )
                     THEN Subst ⌜(n + 1) + (k - 1) ~ n + k⌝ (-1)⋅
                     THEN Auto)⋅
               )⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}F:Top.  \mforall{}L1,L2:\mBbbZ{}  {}\mrightarrow{}  Base.  \mforall{}m:\mBbbN{}.
    ((\mforall{}j:\mBbbN{}m  +  1.  (L1  j  \msim{}  L2  j))  {}\mRightarrow{}  (simple-cbva-seq(L1;F;m)  \msim{}  simple-cbva-seq(L2;F;m)))


By

---

Latex:
(RepeatFor  5  (TACTIC:(D  0  THENA  Auto))
  THEN  RepUR  ``simple-cbva-seq  cbva-seq``  0
  THEN  AutoSplit
  THEN  Try  (HypSubst'  (-1)  0)
  THEN  Try  (Complete  ((RecUnfold  `callbyvalueall-seq`  0  THEN  AutoSplit)))
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  [1;4]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}v  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RenameVar  `n'  (-3)
  THEN  Thin  (-2)
  THEN  (GenConclAtAddrType  \mkleeneopen{}Top\mkleeneclose{}  [1;2]\mcdot{}  THENA  Auto)
  THEN  RenameVar  `K'  (-2)
  THEN  Thin  (-1)
  THEN  ((GenConclAtAddrType  \mkleeneopen{}Top\mkleeneclose{}  [1;3]\mcdot{}  THENA  Auto)
              THEN  RenameVar  `G'  (-2)
              THEN  Thin  (-1)
              THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (m  =  (n  +  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
              THEN  D  (-1)
              THEN  MoveToConcl  (-7)
              THEN  HypSubst'  (-1)  0
              THEN  ThinVar  `m'
              THEN  RepeatFor  2  (MoveToConcl  (-3))
              THEN  NatInd  (-1)
              THEN  ((UnivCD  THENA  Auto)
                          THEN  (RecUnfold  `callbyvalueall-seq`  0
                                      THEN  AutoSplit
                                      THEN  MemCD
                                      THEN  Try  (Complete  ((RWO  "-1"  0  THEN  Auto)))
                                      THEN  (InstHyp  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}f.(K  f  v)\mkleeneclose{}]  (-6)\mcdot{}
                                                  THENA  (Try  (Complete  (Auto))
                                                                THEN  Subst  \mkleeneopen{}(n  +  1)  +  (k  -  1)  \msim{}  n  +  k\mkleeneclose{}  0\mcdot{}
                                                                THEN  Auto)
                                                  )
                                      THEN  Subst  \mkleeneopen{}(n  +  1)  +  (k  -  1)  \msim{}  n  +  k\mkleeneclose{}  (-1)\mcdot{}
                                      THEN  Auto)\mcdot{}
                          )\mcdot{})\mcdot{})

---

Home Index