Nuprl - Pf M_DASH_C_DASH_S_SPACE

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

1. E: TaggedEventStruct
2. P: (|E| List)Prop
3. I: (|E| List)Prop
4. memorylessR(E) preserves P
5. (ternary) composableR(E) preserves P
6. safetyR(E) preserves P
7. safetyR(E) preserves I
8. tr:|E| List. I(tr) tr = nil (L_1,L_2:|E| List. tr = (L_1 @ L_2) & L_2 = nil & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m)))
9. n:
10. 0 < n
11. tr:|E| List. ||tr||n-1 (m:Label. P( < tr > _m)) I(tr) P(tr)

tr:|E| List. ||tr||n (m:Label. P( < tr > _m)) I(tr) P(tr)

By: Auto THEN Decide null(tr) THEN RW assert_pushdownC -1 THEN Unfold `guard` 0 THEN Try (HypSubst -1 0)

Generated subgoals:

1 12. tr: |E| List
13. ||tr||n
14. tr = nil
15. m:Label. P( < nil > _m)
16. I(nil)
P(nil)

2 12. tr: |E| List
13. ||tr||n
14. tr = nil
(m:Label. P( < tr > _m)) I(tr) P(tr)

About:

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

1	12. `tr:` `\|E\| List` 13. `\|\|tr\|\|n` 14. `tr = nil` 15. `m:Label. P( < nil > _m)` 16. `I(nil)` `P(nil)`
2	12. `tr:` `\|E\| List` 13. `\|\|tr\|\|n` 14. `tr = nil` `(m:Label. P( < tr > _m)) I(tr) P(tr)`