---

Step * of Lemma sqeq-copath4

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

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

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index