Step * 1 of Lemma p-compose_wf


1. Type
2. Type
3. Type
4. A ⟶ (B Top)
5. B ⟶ (C Top)
6. A
7. ¬↑can-apply(g;x)
⊢ x ∈ Top
BY
((MoveToConcl (-1))
   THEN Unfold `can-apply` 0
   THEN ((GenConclAtAddr [1; 1; 1; 1]) THENA Auto)
   THEN -2
   THEN Reduce 0
   THEN Auto)⋅ }


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  g  :  A  {}\mrightarrow{}  (B  +  Top)
5.  f  :  B  {}\mrightarrow{}  (C  +  Top)
6.  x  :  A
7.  \mneg{}\muparrow{}can-apply(g;x)
\mvdash{}  g  x  \mmember{}  C  +  Top


By


Latex:
((MoveToConcl  (-1))
  THEN  Unfold  `can-apply`  0
  THEN  ((GenConclAtAddr  [1;  1;  1;  1])  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)\mcdot{}




Home Index