Nuprl - Proof: maximal-in-list 1

(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

1. A : Type
2. f : A

3. A List
4. u : A
5. v : A List
6. 0<||v||

(

a

v.(

x

v.f(x)

f(a)))
7. 0<||v||+1

(

a

[u / v].(

x

[u / v].f(x)

f(a)))

By:

DVar `v'

Generated subgoals:

1 5. 0<||nil||  (anil.(xnil.f(x)f(a)))
6. 0<||nil||+1
  (a[u].(x[u].f(x)f(a)))
3 steps

2 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)))
5 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