(16steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rdist-property 1 1 1 1
1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. (k.x.n(x)^k+1(i) = j)  
  n:. x.n(x)^n+1(i) = j
By: DupHyp -2 THEN Unfold `ring` -1 THEN ExRepD THEN InstHyp [i;j] -2 THEN ExRepD
THEN
InstConcl [k-1]
THEN
Try (DoSubsume THEN Analyze 0 THEN Analyze -1)
THEN
Subst ((k-1+1) ~ k) 0
THENL
[Auto;Id]
THEN
RW assert_pushdownC 0
THEN
Try (DoSubsume THEN Analyze 0 THEN Analyze -1)
THEN
Unfold `rnext` 0
THEN
Trivial

Generated subgoals:

None

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

(16steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc