---

Step * of Lemma sqeq-copath3

∀[a,b,c,f:Top]. ∀[n,m:ℤ].
  (λx.if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x] ~ λx.if (x) < (m)
                                                                         then if x=n then f a[x] else (f b[x])
                                                                         else c[x])
BY
{ ((UnivCD THENA Auto) THEN SqEqCD THEN SqequalSqle THEN SqLeTopToBase THEN AssumeHasValue) }

1
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. (if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x])↓
⊢ if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x] ≤ if (x) < (m)
                                                                  then if x=n then f a[x] else (f b[x])
                                                                  else c[x]

2
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x])
⊢ if (x) < (m)  then f if x=n then a[x] else b[x]  else c[x] ≤ if (x) < (m)
                                                                  then if x=n then f a[x] else (f b[x])
                                                                  else c[x]

3
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. (if (x) < (m)  then if x=n then f a[x] else (f b[x])  else c[x])↓
⊢ if (x) < (m)  then if x=n then f a[x] else (f b[x])  else c[x] ≤ if (x) < (m)
                                                                      then f if x=n then a[x] else b[x]
                                                                      else c[x]

4
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m)  then if x=n then f a[x] else (f b[x])  else c[x])
⊢ if (x) < (m)  then if x=n then f a[x] else (f b[x])  else c[x] ≤ if (x) < (m)
                                                                      then f if x=n then a[x] else b[x]
                                                                      else c[x]

---

Latex:

---

Latex:
\mforall{}[a,b,c,f:Top].  \mforall{}[n,m:\mBbbZ{}].
    (\mlambda{}x.if  (x)  <  (m)    then  f  if  x=n  then  a[x]  else  b[x]    else  c[x]  \msim{}  \mlambda{}x.if  (x)  <  (m)
                                                                                                                                                  then  if  x=n
                                                                                                                                                            then  f  a[x]
                                                                                                                                                            else  (f  b[x])
                                                                                                                                                  else  c[x])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SqEqCD  THEN  SqequalSqle  THEN  SqLeTopToBase  THEN  AssumeHasValue)

---

Home Index