Nuprl - Pf msg_eq

(5steps) PrintForm Definitions Lemmas mb structures Sections GenAutomata Doc

M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)

By: Analyze 0 THEN Inst Thm* E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2) [cEQ(M)] THEN Unfolds [`equiv_rel`;`msg_eq`] 0 THEN Unfolds [`refl`;`sym`;`trans`] 0 THEN Reduce 0 THEN All (RW assert_pushdownC) THEN Try (Complete UseEquiv)

Generated subgoals:

1 1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
sender(M)(a) = sender(M)(a)

2 1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
4. b: |M|
5. (content(M)(a)) =(cEQ(M)) (content(M)(b))
6. sender(M)(a) = sender(M)(b)
7. uid(M)(a) = uid(M)(b)
sender(M)(b) = sender(M)(a)

3 1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
4. b: |M|
5. c: |M|
6. (content(M)(a)) =(cEQ(M)) (content(M)(b))
7. sender(M)(a) = sender(M)(b)
8. uid(M)(a) = uid(M)(b)
9. (content(M)(b)) =(cEQ(M)) (content(M)(c))
10. sender(M)(b) = sender(M)(c)
11. uid(M)(b) = uid(M)(c)
(content(M)(a)) =(cEQ(M)) (content(M)(c))

4 1. M: MessageStruct
2. EquivRel(|cEQ(M)|)(_1 =(cEQ(M)) _2)
3. a: |M|
4. b: |M|
5. c: |M|
6. (content(M)(a)) =(cEQ(M)) (content(M)(b))
7. sender(M)(a) = sender(M)(b)
8. uid(M)(a) = uid(M)(b)
9. (content(M)(b)) =(cEQ(M)) (content(M)(c))
10. sender(M)(b) = sender(M)(c)
11. uid(M)(b) = uid(M)(c)
sender(M)(a) = sender(M)(c)

About:

(5steps) PrintForm Definitions Lemmas mb structures Sections GenAutomata Doc

1	1. `M:` `MessageStruct` 2. `EquivRel(\|cEQ(M)\|)(_1 =(cEQ(M)) _2)` 3. `a:` `\|M\|` `sender(M)(a) = sender(M)(a)`
2	1. `M:` `MessageStruct` 2. `EquivRel(\|cEQ(M)\|)(_1 =(cEQ(M)) _2)` 3. `a:` `\|M\|` 4. `b:` `\|M\|` 5. `(content(M)(a)) =(cEQ(M)) (content(M)(b))` 6. `sender(M)(a) = sender(M)(b)` 7. `uid(M)(a) = uid(M)(b)` `sender(M)(b) = sender(M)(a)`
3	1. `M:` `MessageStruct` 2. `EquivRel(\|cEQ(M)\|)(_1 =(cEQ(M)) _2)` 3. `a:` `\|M\|` 4. `b:` `\|M\|` 5. `c:` `\|M\|` 6. `(content(M)(a)) =(cEQ(M)) (content(M)(b))` 7. `sender(M)(a) = sender(M)(b)` 8. `uid(M)(a) = uid(M)(b)` 9. `(content(M)(b)) =(cEQ(M)) (content(M)(c))` 10. `sender(M)(b) = sender(M)(c)` 11. `uid(M)(b) = uid(M)(c)` `(content(M)(a)) =(cEQ(M)) (content(M)(c))`
4	1. `M:` `MessageStruct` 2. `EquivRel(\|cEQ(M)\|)(_1 =(cEQ(M)) _2)` 3. `a:` `\|M\|` 4. `b:` `\|M\|` 5. `c:` `\|M\|` 6. `(content(M)(a)) =(cEQ(M)) (content(M)(b))` 7. `sender(M)(a) = sender(M)(b)` 8. `uid(M)(a) = uid(M)(b)` 9. `(content(M)(b)) =(cEQ(M)) (content(M)(c))` 10. `sender(M)(b) = sender(M)(c)` 11. `uid(M)(b) = uid(M)(c)` `sender(M)(a) = sender(M)(c)`