Step * of Lemma lifting-strict-less

[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c,d:Top].  (F[if (a) < (b)  then c  else d;p;q;r] if (a) < (b)  then F[c;p;q;r]  else F[d;p;q;r]) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
SqReasoning }

1
1. Base
2. ∀x,y,z,w:Base.  ((F[x;y;z;w])↓  (x)↓)
3. ∀u,v,y,z,w:Base.  (F[exception(u; v);y;z;w] exception(u; v))
4. ∀x,y,z,w:Base.  (is-exception(F[x;y;z;w])  (↓is-exception(x) ∨ (x)↓))
5. Base
6. Base
7. Base
8. Base
9. Base
10. Base
11. Base
12. is-exception(F[if (a) < (b)  then c  else d;p;q;r])
13. is-exception(if (a) < (b)  then c  else d)
14. a ∈ ℤ
15. is-exception(b)
⊢ F[if (a) < (b)  then c  else d;p;q;r] ≤ if (a) < (b)  then F[c;p;q;r]  else F[d;p;q;r]

2
1. Base
2. strict4(λx,y,z,w. F[x;y;z;w])
3. Base
4. Base
5. Base
6. Base
7. Base
8. Base
9. Base
10. is-exception(if (a) < (b)  then F[c;p;q;r]  else F[d;p;q;r])
11. a ∈ ℤ
12. is-exception(b)
⊢ if (a) < (b)  then F[c;p;q;r]  else F[d;p;q;r] ≤ F[if (a) < (b)  then c  else d;p;q;r]


Latex:


Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,b,c,d:Top].
        (F[if  (a)  <  (b)    then  c    else  d;p;q;r]  \msim{}  if  (a)  <  (b)    then  F[c;p;q;r]    else  F[d;p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By


Latex:
SqReasoning




Home Index