Step
*
2
4
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))
(l @ []))↓@i
6. (l @ [])↓@i
7. (l @ [])↓
8. ∀a,b:Top. (if l @ [] is a pair then a otherwise b ~ b)
9. ∀a,b:Top. (if l @ [] is inl then a else b ~ b)
10. ∀a,b:Top. (if l @ [] is inr then a else b ~ b)
⊢ l ≤ l @ []
BY
{ ((InstLemma `ispair-or-isaxiom-append-nil` [⌜l⌝]⋅ THENA Auto)
THEN All(\i.(InstHyp [⌜tt⌝;⌜ff⌝] i⋅ THENA CpltAuto))⋅
THEN All(\i.(RWO "sqeqff_to_assert" i THENA CanonicalAuto))⋅
THEN All(\i.(RW assert_pushdownC i THENA CanonicalAuto))⋅
THEN D (-4)
THEN (Auto THEN Try (ComputeSameException 100))
THEN Try (((FLemma `isaxiom-append-nil` [-5] THENA Auto)
THEN Duplicate (-6)
THEN HVimplies (-1) [1]
THEN Duplicate (-3)
THEN HVimplies (-1) [1])))⋅ }
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))
(l @ []))\mdownarrow{}@i
6. (l @ [])\mdownarrow{}@i
7. (l @ [])\mdownarrow{}
8. \mforall{}a,b:Top. (if l @ [] is a pair then a otherwise b \msim{} b)
9. \mforall{}a,b:Top. (if l @ [] is inl then a else b \msim{} b)
10. \mforall{}a,b:Top. (if l @ [] is inr then a else b \msim{} b)
\mvdash{} l \mleq{} l @ []
By
Latex:
((InstLemma `ispair-or-isaxiom-append-nil` [\mkleeneopen{}l\mkleeneclose{}]\mcdot{} THENA Auto)
THEN All(\mbackslash{}i.(InstHyp [\mkleeneopen{}tt\mkleeneclose{};\mkleeneopen{}ff\mkleeneclose{}] i\mcdot{} THENA CpltAuto))\mcdot{}
THEN All(\mbackslash{}i.(RWO "sqeqff\_to\_assert" i THENA CanonicalAuto))\mcdot{}
THEN All(\mbackslash{}i.(RW assert\_pushdownC i THENA CanonicalAuto))\mcdot{}
THEN D (-4)
THEN (Auto THEN Try (ComputeSameException 100))
THEN Try (((FLemma `isaxiom-append-nil` [-5] THENA Auto)
THEN Duplicate (-6)
THEN HVimplies (-1) [1]
THEN Duplicate (-3)
THEN HVimplies (-1) [1])))\mcdot{}
Home
Index