Nuprl - Proof: maximal-in-list 1 2

(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: maximal-in-list 1 2

1. A : Type
2. f : A

3. A List
4. u : A
5. u1 : A
6. v1 : A List
7. 0<||[u1 / v1]||

(

a

[u1 / v1].(

x

[u1 / v1].f(x)

f(a)))
8. 0<||[u1 / v1]||+1

(

a

[u; u1 / v1].(

x

[u; u1 / v1].f(x)

f(a)))

By:	Analyze -2 THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) (yL.P(y)) 0 THEN DupHyp -1 THEN Analyze -1 THEN Decide (f(a)f(u)) THENL [OrLeft;OrRight]

Generated subgoals:

1 7. 0<||[u1 / v1]||+1
8. (a[u1 / v1].(x[u1 / v1].f(x)f(a)))
9. a : A
10. (a  [u1 / v1])
11. (x[u1 / v1].f(x)f(a))
12. f(a)f(u)
  (x[u; u1 / v1].f(x)f(u))
2 steps

2 7. 0<||[u1 / v1]||+1
8. (a[u1 / v1].(x[u1 / v1].f(x)f(a)))
9. a : A
10. (a  [u1 / v1])
11. (x[u1 / v1].f(x)f(a))
12. f(a)f(u)
  (a[u1 / v1].(x[u; u1 / v1].f(x)f(a)))
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc