Step * of Lemma lifting-strict-atom_eq

[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c,d:Top].  (F[if a=b then else fi ;p;q;r] if a=b then F[c;p;q;r] else F[d;p;q;r] fi 
  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 else fi ;p;q;r])
13. is-exception(if a=b then else fi )
14. a ∈ Atom
15. is-exception(b)
⊢ F[if a=b then else fi ;p;q;r] ≤ if a=b then F[c;p;q;r] else F[d;p;q;r] fi 

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] fi )
11. a ∈ Atom
12. is-exception(b)
⊢ if a=b then F[c;p;q;r] else F[d;p;q;r] fi  ≤ F[if a=b then else fi ;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  fi  ;p;q;r]  \msim{}  if  a=b  then  F[c;p;q;r]  else  F[d;p;q;r]  fi  ) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By


Latex:
SqReasoning




Home Index