Step
*
2
1
of Lemma
evalall-append-nil
1. j : ℤ
2. 0 < j
3. ∀l:Base
((fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ []))↓
⇒ (λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x^j - 1
⊥
(l @ []))↓
⇒ (l ≤ fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr
eval y = evalall outr(x) in
inr y
else x))
(l @ [])))
4. l : Base@i
5. (fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
<fst((l @ [])), snd((l @ []))>)↓@i
6. (eval a' = λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x^j - 1
⊥
(fst((l @ []))) in
eval b' = λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x^j - 1
⊥
(snd((l @ []))) in
<a', b'>)↓@i
7. 0 ≤ 0
8. l @ [] ~ <fst((l @ [])), snd((l @ []))>
⊢ l ≤ eval a' = fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(fst((l @ []))) in
eval b' = fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(snd((l @ []))) in
<a', b'>
BY
{ (HasValueD (-3)
THEN HasValueD (-4)
THEN (InstLemma `pi1-if-ispair-append-nil` [⌜l⌝]⋅ THENA (Auto THEN HypSubst (-3) 0 THEN Auto))
THEN (InstLemma `pi2-if-ispair-append-nil` [⌜l⌝]⋅ THENA (Auto THEN HypSubst (-4) 0 THEN Auto))
THEN RW UnrollLoopsC (-8)
THEN Reduce (-8)
THEN HasValueD (-8)
THEN (HasValueD (-9)
THEN (InstLemma `prod-if-ispair-append-nil` [⌜l⌝]⋅ THENA (Auto THEN HypSubst (-7) 0 THEN Auto))
THEN UsePairEta [1] 0
THEN SqLeCD
THEN RepUR ``cons`` 0
THEN Try (Complete ((BackThruSomeHyp THEN RevHypSubst (-4) 0 THEN Auto)))
THEN All (Fold `evalall`)
THEN HypSubst (-5) (-3)
THEN RWO "evalall-sqequal" 0
THEN Auto)⋅) }
Latex:
Latex:
1. j : \mBbbZ{}
2. 0 < j
3. \mforall{}l:Base
((fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ []))\mdownarrow{}
{}\mRightarrow{} (\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(l @ []))\mdownarrow{}
{}\mRightarrow{} (l \mleq{} fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(l @ [])))
4. l : Base@i
5. (fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
<fst((l @ [])), snd((l @ []))>)\mdownarrow{}@i
6. (eval a' = \mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(fst((l @ []))) in
eval b' = \mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x\^{}j - 1
\mbot{}
(snd((l @ []))) in
<a', b'>)\mdownarrow{}@i
7. 0 \mleq{} 0
8. l @ [] \msim{} <fst((l @ [])), snd((l @ []))>
\mvdash{} l \mleq{} eval a' = fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(fst((l @ []))) in
eval b' = fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'>
otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
(snd((l @ []))) in
<a', b'>
By
Latex:
(HasValueD (-3)
THEN HasValueD (-4)
THEN (InstLemma `pi1-if-ispair-append-nil` [\mkleeneopen{}l\mkleeneclose{}]\mcdot{} THENA (Auto THEN HypSubst (-3) 0 THEN Auto))
THEN (InstLemma `pi2-if-ispair-append-nil` [\mkleeneopen{}l\mkleeneclose{}]\mcdot{} THENA (Auto THEN HypSubst (-4) 0 THEN Auto))
THEN RW UnrollLoopsC (-8)
THEN Reduce (-8)
THEN HasValueD (-8)
THEN (HasValueD (-9)
THEN (InstLemma `prod-if-ispair-append-nil` [\mkleeneopen{}l\mkleeneclose{}]\mcdot{}
THENA (Auto THEN HypSubst (-7) 0 THEN Auto)
)
THEN UsePairEta [1] 0
THEN SqLeCD
THEN RepUR ``cons`` 0
THEN Try (Complete ((BackThruSomeHyp THEN RevHypSubst (-4) 0 THEN Auto)))
THEN All (Fold `evalall`)
THEN HypSubst (-5) (-3)
THEN RWO "evalall-sqequal" 0
THEN Auto)\mcdot{})
Home
Index