Nuprl - Pf min_el

PrintForm Definitions choice 1 Sections AutomataTheory Doc

E:(), n,k:. (EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk })

By: UnivCD THEN Analyze 0

Generated subgoals:

1 1. E:
2. n:
3. k:
4. EquivRel x,y:. x E y
(n E k) Min{ x | xEn } = Min{ x | xEk }

2 1. E:
2. n:
3. k:
4. EquivRel x,y:. x E y
n E k (Min{ x | xEn } = Min{ x | xEk })

About:

1	1. `E:` 2. `n:` 3. `k:` 4. `EquivRel x,y:. x E y` `(n E k) Min{ x \| xEn } = Min{ x \| xEk }`
2	1. `E:` 2. `n:` 3. `k:` 4. `EquivRel x,y:. x E y` `n E k (Min{ x \| xEn } = Min{ x \| xEk })`