---

Step * of Lemma cbva_seq-sqequal-n

∀L:Top. ∀F1,F2:Base. ∀m,n:ℕ.  ((F1 ~n + 1 F2) ⇒ (cbva_seq(L; F1; m) ~n cbva_seq(L; F2; m)))
BY
{ (((UnivCD THENA Auto') THEN SqEqualNTopToBase THEN PromoteHyp (-1) 1)
   THEN RepUR ``cbva_seq`` 0
   THEN ((Assert ⌜∃K:Base. True⌝⋅ THENA (InstConcl [⌜1⌝]⋅ THEN Auto))
         THEN D (-1)
         THEN Thin (-1)
         THEN (Subst ⌜λx.x ~ λx.mk_applies(x;K;0)⌝ 0⋅ THENA (RepUR ``mk_applies`` 0 THEN Auto))
         THEN (GenConclAtAddrType ⌜ℕ⌝ [2;4]⋅ THENA Auto)
         THEN (Assert ⌜v ≤ m⌝⋅ THENA Auto)
         THEN Thin (-2)
         THEN (Assert ⌜∃j:ℕ. (m = (v + j) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - v⌝]⋅ THEN Auto'))
         THEN D (-1)
         THEN HypSubst' (-1) 0
         THEN ThinVar `m'
         THEN RepeatFor 2 (MoveToConcl (-2))
         THEN NatInd (-1)
         THEN (UnivCD THENA Auto')
         THEN Try (Complete ((RecUnfold `callbyvalueall_seq` 0 THEN AutoSplit THEN SqequalNNonCanonicalCD⋅ THEN Auto)))
         THEN RecUnfold `callbyvalueall_seq` 0
         THEN AutoSplit
         THEN Try (Complete (Auto'))
         THEN SqequalNNonCanonicalCD⋅
         THEN Try (Complete (Auto))
         THEN (InstHyp [⌜λi.if (i =z v) then v1 else K i fi ⌝;⌜v + 1⌝] (-5)⋅ THENA Auto)
         THEN (Subst ⌜(v + 1) + (j - 1) ~ v + j⌝ (-1)⋅ THENA Auto)
         THEN RWO "mk_applies_roll" 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}L:Top.  \mforall{}F1,F2:Base.  \mforall{}m,n:\mBbbN{}.    ((F1  \msim{}n  +  1  F2)  {}\mRightarrow{}  (cbva\_seq(L;  F1;  m)  \msim{}n  cbva\_seq(L;  F2;  m)))


By

---

Latex:
(((UnivCD  THENA  Auto')  THEN  SqEqualNTopToBase  THEN  PromoteHyp  (-1)  1)
  THEN  RepUR  ``cbva\_seq``  0
  THEN  ((Assert  \mkleeneopen{}\mexists{}K:Base.  True\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THEN  Auto))
              THEN  D  (-1)
              THEN  Thin  (-1)
              THEN  (Subst  \mkleeneopen{}\mlambda{}x.x  \msim{}  \mlambda{}x.mk\_applies(x;K;0)\mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``mk\_applies``  0  THEN  Auto))
              THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  [2;4]\mcdot{}  THENA  Auto)
              THEN  (Assert  \mkleeneopen{}v  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-2)
              THEN  (Assert  \mkleeneopen{}\mexists{}j:\mBbbN{}.  (m  =  (v  +  j))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  v\mkleeneclose{}]\mcdot{}  THEN  Auto'))
              THEN  D  (-1)
              THEN  HypSubst'  (-1)  0
              THEN  ThinVar  `m'
              THEN  RepeatFor  2  (MoveToConcl  (-2))
              THEN  NatInd  (-1)
              THEN  (UnivCD  THENA  Auto')
              THEN  Try  (Complete  ((RecUnfold  `callbyvalueall\_seq`  0
                                                        THEN  AutoSplit
                                                        THEN  SqequalNNonCanonicalCD\mcdot{}
                                                        THEN  Auto)))
              THEN  RecUnfold  `callbyvalueall\_seq`  0
              THEN  AutoSplit
              THEN  Try  (Complete  (Auto'))
              THEN  SqequalNNonCanonicalCD\mcdot{}
              THEN  Try  (Complete  (Auto))
              THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  v)  then  v1  else  K  i  fi  \mkleeneclose{};\mkleeneopen{}v  +  1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
              THEN  (Subst  \mkleeneopen{}(v  +  1)  +  (j  -  1)  \msim{}  v  +  j\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
              THEN  RWO  "mk\_applies\_roll"  0
              THEN  Auto)\mcdot{})

---

Home Index