---

Step * 1 of Lemma simple-cbva-seq-list-case2


1. F : Top
2. L1 : Top
3. L2 : Top
4. G : Top
5. a : Top
6. m1 : ℕ+
7. m2 : ℕ
⊢ callbyvalueall-seq(λn.if (n) < (m1)
                           then L1 a n
                           else mk_lambdas(λout.if n - m1=m2
                                                then mk_lambdas(λo1.G[out;o1];m2 - 1)
                                                else (L2 a (n - m1));m1 - 1);λx.x;mk_lambdas(F;((m1 + m2) + 1) - 1);0
                     ;(m1 + m2) + 1) 
~ callbyvalueall-seq(λn.if (n) < (m1)
                           then L1 a n
                           else if (n) < (m1 + m2)
                                   then mk_lambdas(L2 a (n - m1);m1)
                                   else mk_lambdas(λout1.mk_lambdas(λout2.G[out1;out2];m2 - 1);m1 - 1);λx.x
                     ;mk_lambdas(F;((m1 + m2) + 1) - 1);0;(m1 + m2) + 1)
BY
{ TACTIC:(TACTIC:(Subst ⌜((m1 + m2) + 1) - 1 ~ m1 + m2⌝ 0⋅ THENA Auto)
          THEN (RWO "callbyvalueall_seq-seq" 0 THENA Auto')
          THEN (Subst ⌜λx.x ~ λf.mk_applies(f;λx.x;0)⌝ 0⋅ THENA (RepUR ``mk_applies`` 0 THEN Auto))
          THEN (RWO "callbyvalueall_seq-decomp-last" 0 THENA Auto')
          THEN Reduce 0
          THEN (Subst ⌜((m1 + m2) + 1) - 1 ~ m1 + m2⌝ 0⋅ THENA Auto)
          THEN (Subst ⌜(m1 + m2) - m1 ~ m2⌝ 0⋅ THENA Auto)
          THEN (RW (SubC (AddrC [3] (SweepUpC (LemmaC `less_as_ite`)))) 0 THENA Auto)⋅
          THEN Repeat (AutoSplit)
          THEN Try (Complete (Auto'))
          THEN ((GenConclAtAddrType ⌜Top⌝ [1;3]⋅ THENA Auto) THEN Thin (-1) THEN RenameVar `X' (-1)⋅)⋅) }

1
1. F : Top
2. L1 : Top
3. L2 : Top
4. G : Top
5. a : Top
6. m1 : ℕ+
7. m2 : ℕ
8. ¬m1 + m2 < m1 + m2
9. ¬m1 + m2 < m1
10. X : Top
⊢ callbyvalueall_seq(λn.if (n) < (m1)
                           then L1 a n
                           else mk_lambdas(λout.if n - m1=m2
                                                then mk_lambdas(λo1.G[out;o1];m2 - 1)
                                                else (L2 a (n - m1));m1 - 1);λf.mk_applies(f;λx.x;0);X;0;m1 + m2) 
~ callbyvalueall_seq(λn.if (n) < (m1)
                           then L1 a n
                           else if (n) < (m1 + m2)
                                   then mk_lambdas(L2 a (n - m1);m1)
                                   else mk_lambdas(λout1.mk_lambdas(λout2.G[out1;out2];m2 - 1);m1 - 1)
                    ;λf.mk_applies(f;λx.x;0);X;0;m1 + m2)

---

Latex:

---

Latex:

1.  F  :  Top
2.  L1  :  Top
3.  L2  :  Top
4.  G  :  Top
5.  a  :  Top
6.  m1  :  \mBbbN{}\msupplus{}
7.  m2  :  \mBbbN{}
\mvdash{}  callbyvalueall-seq(\mlambda{}n.if  (n)  <  (m1)
                                                      then  L1  a  n
                                                      else  mk\_lambdas(\mlambda{}out.if  n  -  m1=m2
                                                                                                then  mk\_lambdas(\mlambda{}o1.G[out;o1];m2  -  1)
                                                                                                else  (L2  a  (n  -  m1));m1  -  1);\mlambda{}x.x;mk\_lambdas(F;((m1
                                          +  m2)
                                          +  1)  -  1);0;(m1  +  m2)  +  1) 
\msim{}  callbyvalueall-seq(\mlambda{}n.if  (n)  <  (m1)
                                                      then  L1  a  n
                                                      else  if  (n)  <  (m1  +  m2)
                                                                      then  mk\_lambdas(L2  a  (n  -  m1);m1)
                                                                      else  mk\_lambdas(\mlambda{}out1.mk\_lambdas(\mlambda{}out2.G[out1;out2];m2  -  1);m1 
                                                                                -  1);\mlambda{}x.x;mk\_lambdas(F;((m1  +  m2)  +  1)  -  1);0;(m1  +  m2)  +  1)


By

---

Latex:
TACTIC:(TACTIC:(Subst  \mkleeneopen{}((m1  +  m2)  +  1)  -  1  \msim{}  m1  +  m2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                THEN  (RWO  "callbyvalueall\_seq-seq"  0  THENA  Auto')
                THEN  (Subst  \mkleeneopen{}\mlambda{}x.x  \msim{}  \mlambda{}f.mk\_applies(f;\mlambda{}x.x;0)\mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``mk\_applies``  0  THEN  Auto))
                THEN  (RWO  "callbyvalueall\_seq-decomp-last"  0  THENA  Auto')
                THEN  Reduce  0
                THEN  (Subst  \mkleeneopen{}((m1  +  m2)  +  1)  -  1  \msim{}  m1  +  m2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                THEN  (Subst  \mkleeneopen{}(m1  +  m2)  -  m1  \msim{}  m2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                THEN  (RW  (SubC  (AddrC  [3]  (SweepUpC  (LemmaC  `less\_as\_ite`))))  0  THENA  Auto)\mcdot{}
                THEN  Repeat  (AutoSplit)
                THEN  Try  (Complete  (Auto'))
                THEN  ((GenConclAtAddrType  \mkleeneopen{}Top\mkleeneclose{}  [1;3]\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  RenameVar  `X'  (-1)\mcdot{})
                \mcdot{})

---

Home Index