Nuprl - Proof: fpf-sub-functionality

(22steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-sub-functionality

A,A':Type.

strong-subtype(A;A')

(

B:(A

Type), C:(A'

Type), eq:EqDecider(A), eq':EqDecider(A'),

(

f,g:a:A fp-> B(a). (

a:A. B(a)

r C(a))

By:	Repeat (Analyze 0 THENA Complete Auto) THEN AssertBY (A r A') (Analyze 3 THEN Trivial) THEN AssertBY (eq' EqDecider(A)) (DoSubsume (THEN (BackThru Thm* strong-subtype(A;B) (EqDecider(B) r EqDecider(A))) THEN Analyze 0 THENA (Auto THEN TrySubsume) THEN ParallelOp -1 THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 1. A : Type
2. A' : Type
3. strong-subtype(A;A')
4. B : AType
5. C : A'Type
6. eq : EqDecider(A)
7. eq' : EqDecider(A')
8. f : a:A fp-> B(a)
9. g : a:A fp-> B(a)
10. A r A'
11. eq'  EqDecider(A)
12. a:A. B(a) r C(a)
13. x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)
14. x : A
15. x  dom(f)
  x  dom(g) & f(x) = g(x)  C(x)
20 steps

2 1. A : Type{i}
2. A' : Type{i}
3. strong-subtype(A;A')
4. B : AType{i}
5. C : A'Type{i}
6. eq : EqDecider(A)
7. eq' : EqDecider(A')
8. f : a:A fp-> B(a)
9. g : a:A fp-> B(a)
10. A r A'
11. eq'  EqDecider(A)
12. a:A. B(a) r C(a)
13. x:A. x  dom(f)  x  dom(g) & f(x) = g(x)  B(x)
14. x : A
  x  dom(f)  Prop{1}
1 step

About:

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

(22steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc

1	1. A : Type 2. A' : Type 3. strong-subtype(A;A') 4. B : AType 5. C : A'Type 6. eq : EqDecider(A) 7. eq' : EqDecider(A') 8. f : a:A fp-> B(a) 9. g : a:A fp-> B(a) 10. A r A' 11. eq' EqDecider(A) 12. a:A. B(a) r C(a) 13. x:A. x dom(f) x dom(g) & f(x) = g(x) B(x) 14. x : A 15. x dom(f) x dom(g) & f(x) = g(x) C(x)	20 steps
2	1. A : Type{i} 2. A' : Type{i} 3. strong-subtype(A;A') 4. B : AType{i} 5. C : A'Type{i} 6. eq : EqDecider(A) 7. eq' : EqDecider(A') 8. f : a:A fp-> B(a) 9. g : a:A fp-> B(a) 10. A r A' 11. eq' EqDecider(A) 12. a:A. B(a) r C(a) 13. x:A. x dom(f) x dom(g) & f(x) = g(x) B(x) 14. x : A x dom(f) Prop{1}	1 step