Step |
Hyp |
Ref |
Expression |
1 |
|
bnj126.1 |
|
2 |
|
bnj126.2 |
Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |- |
3 |
|
bnj126.3 |
Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |- |
4 |
|
bnj126.4 |
|
5 |
2
|
sbcbii |
Could not format ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) : No typesetting found for |- ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) with typecode |- |
6 |
4
|
bnj95 |
|
7 |
1 6
|
bnj106 |
|
8 |
3 5 7
|
3bitri |
Could not format ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) with typecode |- |