Nuprl - Proof: w-pred-aux

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-pred-aux

the_w:World, t:

, i:Id.

first(<i,t>)

pred(<i,t>)

E

By:	InductionOnNat THEN RecUnfold `w-first` 0 THEN RecUnfold `w-pred` 0 THEN Unfolds [`w-loc`;`w-time`] 0 THEN Reduce 0 THEN Try (Complete (Auto THEN Analyze -1)) THEN SplitOnConclITE

Generated subgoals:

1 1. the_w : World
2. t :
3. 0<t
4. i:Id. first(<i,t-1>)  pred(<i,t-1>)  E
5. t = 0
  i:Id. true  if isnull(a(i;t-1)) pred(<i,t-1>) else <i,t-1> fi  E
Auto

2 1. the_w : World
2. t :
3. 0<t
4. i:Id. first(<i,t-1>)  pred(<i,t-1>)  E
5. t=0
  i:Id.
  if isnull(a(i;t-1)) first(<i,t-1>) else false fi

  if isnull(a(i;t-1)) pred(<i,t-1>) else <i,t-1> fi  E
3 steps

About:

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

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