Step * 2 of Lemma message-cmp-zero


1. Name ⟶ Type
2. hdrs Name List
3. mcmp hdr:Name ⟶ comparison(f hdr)
4. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. msg-authentic(x) msg-authentic(y)
∧ (msg-header(x) msg-header(y) ∈ Name)
∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ)
⊢ (message-cmp(hdrs;mcmp) y) 0 ∈ ℤ
BY
(RepUR ``message-cmp`` THEN (RWW "comparison-seq-zero" THEN Try (Fold `message-cmp` 0)) THEN Auto) }

1
1. Name ⟶ Type
2. hdrs Name List
3. mcmp hdr:Name ⟶ comparison(f hdr)
4. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. msg-authentic(x) msg-authentic(y)
7. msg-header(x) msg-header(y) ∈ Name
8. (mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ
9. (compare-fun(bool-cmp();λm.msg-authentic(m)) y) 0 ∈ ℤ
10. (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) y) 0 ∈ ℤ
⊢ msg-body-cmp(mcmp) y ∈ ℤ

2
1. Name ⟶ Type
2. hdrs Name List
3. mcmp hdr:Name ⟶ comparison(f hdr)
4. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. msg-authentic(x) msg-authentic(y)
7. msg-header(x) msg-header(y) ∈ Name
8. (mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ
9. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
10. a@0 {b:{m:Message(f)| (msg-header(m) ∈ hdrs)} (compare-fun(bool-cmp();λm.msg-authentic(m)) b) 0 ∈ ℤ
⊢ msg-body-cmp(mcmp) ∈ comparison({b:{b:{m:Message(f)| (msg-header(m) ∈ hdrs)} 
                                      (compare-fun(bool-cmp();λm.msg-authentic(m)) b) 0 ∈ ℤ
                                   (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) a@0 b) 0 ∈ ℤ)

3
1. Name ⟶ Type
2. hdrs Name List
3. mcmp hdr:Name ⟶ comparison(f hdr)
4. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. msg-authentic(x) msg-authentic(y)
7. msg-header(x) msg-header(y) ∈ Name
8. (mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ
⊢ (compare-fun(bool-cmp();λm.msg-authentic(m)) y) 0 ∈ ℤ

4
1. Name ⟶ Type
2. hdrs Name List
3. mcmp hdr:Name ⟶ comparison(f hdr)
4. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. msg-authentic(x) msg-authentic(y)
7. msg-header(x) msg-header(y) ∈ Name
8. (mcmp msg-header(x) msg-body(x) msg-body(y)) 0 ∈ ℤ
9. (compare-fun(bool-cmp();λm.msg-authentic(m)) y) 0 ∈ ℤ
⊢ (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) y) 0 ∈ ℤ


Latex:


Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  hdrs  :  Name  List
3.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
4.  x  :  \{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\} 
5.  y  :  \{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\} 
6.  msg-authentic(x)  =  msg-authentic(y)
\mwedge{}  (msg-header(x)  =  msg-header(y))
\mwedge{}  ((mcmp  msg-header(x)  msg-body(x)  msg-body(y))  =  0)
\mvdash{}  (message-cmp(hdrs;mcmp)  x  y)  =  0


By


Latex:
(RepUR  ``message-cmp``  0
  THEN  (RWW  "comparison-seq-zero"  0  THEN  Try  (Fold  `message-cmp`  0))
  THEN  Auto)




Home Index