Nuprl - Pf tag_sublist

(4steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

E:TaggedEventStruct. tag_splitable(E;adR(E))

By: Unfolds [`tag_splitable`;`R_ad`] 0 THEN Unfold `str_trace` 0 THEN Unfold `rel_star` -2 THEN Reduce -2 THEN ExRepD THEN MoveToConcl 3 THEN MoveToConcl 2 THEN NatInd -2 THEN RecUnfold `rel_exp` 0 THEN Reduce 0

Generated subgoals:

1 1. E: TaggedEventStruct
2. m: Label
tr_1,tr_2:|E| List. tr_1 = tr_2 ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m)

2 1. E: TaggedEventStruct
2. m: Label
3. n:
4. 0 < n
5. tr_1,tr_2:|E| List. (tr_1 delayableR(E) asyncR(E)^n-1 tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m)
tr_1,tr_2:|E| List. (tr_1 if n=0 x,y. x = y |E| List else x,y. z:|E| List. (x (delayableR(E) asyncR(E)) z) & (z delayableR(E) asyncR(E)^n-1 y) fi tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m)

About:

(4steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

1	1. `E:` `TaggedEventStruct` 2. `m:` `Label` `tr_1,tr_2:\|E\| List. tr_1 = tr_2 ( < tr_1 > _m ((delayableR(E) asyncR(E))^*) < tr_2 > _m)`
2	1. `E:` `TaggedEventStruct` 2. `m:` `Label` 3. `n:` 4. `0 < n` 5. `tr_1,tr_2:\|E\| List. (tr_1 delayableR(E) asyncR(E)^n-1 tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^) < tr_2 > _m)` `tr_1,tr_2:\|E\| List. (tr_1 if n=0 x,y. x = y \|E\| List else x,y. z:\|E\| List. (x (delayableR(E) asyncR(E)) z) & (z delayableR(E) asyncR(E)^n-1 y) fi tr_2) ( < tr_1 > _m ((delayableR(E) asyncR(E))^) < tr_2 > _m)`