---

Step * of Lemma equal-zero-streams

fix((λx.<⋅, x>)) ~ fix((λx.<⋅, ⋅, x>))
BY
{ (SqequalSqle
   THEN OneFixpointLeast
   THEN CompNatInd (-1)
   THEN (Decide ⌜j = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((Eliminate ⌜j⌝⋅ THEN AllReduce THEN Auto)))
   THEN (RW (AddrC [2] UnrollRecursionC) 0 THEN Reduce 0)
   THEN (Decide ⌜j = 1 ∈ ℤ⌝⋅ THENA Auto)
   THEN Try (Complete ((Eliminate ⌜j⌝⋅ THEN AllReduce THEN Auto)))) }

1
1. j : ℕ
2. ∀j:ℕj. (λx.<⋅, x>^j ⊥ ≤ fix((λx.<⋅, ⋅, x>)))
3. ¬(j = 0 ∈ ℤ)
4. ¬(j = 1 ∈ ℤ)
⊢ λx.<⋅, x>^j ⊥ ≤ <⋅, ⋅, fix((λx.<⋅, ⋅, x>))>

2
1. j : ℕ
2. ∀j:ℕj. (λx.<⋅, ⋅, x>^j ⊥ ≤ fix((λx.<⋅, x>)))
3. ¬(j = 0 ∈ ℤ)
4. j = 1 ∈ ℤ
⊢ λx.<⋅, ⋅, x>^j ⊥ ≤ <⋅, fix((λx.<⋅, x>))>

3
1. j : ℕ
2. ∀j:ℕj. (λx.<⋅, ⋅, x>^j ⊥ ≤ fix((λx.<⋅, x>)))
3. ¬(j = 0 ∈ ℤ)
4. ¬(j = 1 ∈ ℤ)
⊢ λx.<⋅, ⋅, x>^j ⊥ ≤ <⋅, fix((λx.<⋅, x>))>

---

Latex:

---

Latex:
fix((\mlambda{}x.<\mcdot{},  x>))  \msim{}  fix((\mlambda{}x.<\mcdot{},  \mcdot{},  x>))


By

---

Latex:
(SqequalSqle
  THEN  OneFixpointLeast
  THEN  CompNatInd  (-1)
  THEN  (Decide  \mkleeneopen{}j  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((Eliminate  \mkleeneopen{}j\mkleeneclose{}\mcdot{}  THEN  AllReduce  THEN  Auto)))
  THEN  (RW  (AddrC  [2]  UnrollRecursionC)  0  THEN  Reduce  0)
  THEN  (Decide  \mkleeneopen{}j  =  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((Eliminate  \mkleeneopen{}j\mkleeneclose{}\mcdot{}  THEN  AllReduce  THEN  Auto))))

---

Home Index