Step * of Lemma cbv-reduce-strict

[F,a,B:Base].
  F[eval in
    B[x]] ≤ F[B[a]] 
  supposing (∀x:Base. ((F[x])↓  (x)↓))
  ∧ (∀u,v,x:Base.  ((F[x] exception(u; v))  (↓(x exception(u; v)) ∨ (x)↓)))
  ∧ (∀u,v:Base.  (B[exception(u; v)] exception(u; v)))
BY
TACTIC:((UnivCD THENA Auto) THEN SplitAndHyps THEN AssumeHasValue) }

1
1. Base
2. Base
3. Base
4. ∀x:Base. ((F[x])↓  (x)↓)
5. ∀u,v,x:Base.  ((F[x] exception(u; v))  (↓(x exception(u; v)) ∨ (x)↓))
6. ∀u,v:Base.  (B[exception(u; v)] exception(u; v))
7. (F[eval in
      B[x]])↓
⊢ F[eval in
    B[x]] ≤ F[B[a]]

2
1. Base
2. Base
3. Base
4. ∀x:Base. ((F[x])↓  (x)↓)
5. ∀u,v,x:Base.  ((F[x] exception(u; v))  (↓(x exception(u; v)) ∨ (x)↓))
6. ∀u,v:Base.  (B[exception(u; v)] exception(u; v))
7. is-exception(F[eval in
                  B[x]])
⊢ F[eval in
    B[x]] ≤ F[B[a]]


Latex:


Latex:
\mforall{}[F,a,B:Base].
    F[eval  x  =  a  in
        B[x]]  \mleq{}  F[B[a]] 
    supposing  (\mforall{}x:Base.  ((F[x])\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{}))
    \mwedge{}  (\mforall{}u,v,x:Base.    ((F[x]  \msim{}  exception(u;  v))  {}\mRightarrow{}  (\mdownarrow{}(x  \msim{}  exception(u;  v))  \mvee{}  (x)\mdownarrow{})))
    \mwedge{}  (\mforall{}u,v:Base.    (B[exception(u;  v)]  \msim{}  exception(u;  v)))


By


Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  SplitAndHyps  THEN  AssumeHasValue)




Home Index