1. l : Base2. (evalall(l @ []))↓⊢ l ≤ evalall(l @ []){ (All (Unfold `evalall`) THEN Compactness (-1) THEN SqUnhide THEN MoveToConcl 1 THEN NatInd (-1) THEN Reduce 0 THEN Strictness THEN Try ((RWO "fun_exp_unroll_1" 0 THENA Auto)) THEN Reduce 0 THEN (UnivCD THENA Auto) THEN BotDiv THEN HasValueD (-1) THEN RW UnrollLoopsC 0 THEN Reduce 0 THEN (CallByValueReduce 0 THENA Trivial) THEN Repeat (HVimplies2 0 [2])) }1. j : ℤ2. 0 < j3. ∀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@i5. (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 @ []))>)↓@i6. (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'>)↓@i7. 0 ≤ 08. 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'>1. j : ℤ2. 0 < j3. ∀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@i5. (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)) (inl outl(l @ [])))↓@i6. (eval y = λ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 ⊥ outl(l @ []) in inl y)↓@i7. 0 ≤ 08. ∀a,b:Top. (b ~ b)9. l @ [] ~ inl outl(l @ [])⊢ l ≤ eval y = 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)) outl(l @ []) in inl y1. j : ℤ2. 0 < j3. ∀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@i5. (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)) (inr outr(l @ []) ))↓@i6. (eval y = λ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 ⊥ outr(l @ []) in inr y )↓@i7. 0 ≤ 08. ∀a,b:Top. (b ~ b)9. ∀a,b:Top. (b ~ b)10. l @ [] ~ inr outr(l @ []) ⊢ l ≤ eval y = 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)) outr(l @ []) in inr y 1. j : ℤ2. 0 < j3. ∀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@i5. (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 @ []))↓@i6. (l @ [])↓@i7. (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 @ []