Nuprl Lemma : decidable__ses-legal-sequence
∀prvt:Atom1. ∀pas:ProtocolAction List. Dec(Legal(pas) given prvt)
Proof
Definitions occuring in Statement :
ses-legal-sequence: Legal(pas) given prvt,
protocol-action: ProtocolAction,
list: T List,
atom: Atom$n,
decidable: Dec(P),
all: ∀x:A. B[x]
Lemmas :
decidable__all_int_seg,
length_wf,
protocol-action_wf,
l_contains_wf,
pa-used_wf,
select_wf,
sq_stable__le,
cons_wf,
concat_wf,
map_wf,
le_wf,
less_than_wf,
list_wf,
pa-useable_wf,
less_than_transitivity2,
le_weakening2,
from-upto_wf,
int_seg_wf,
decidable__l_contains,
decidable__atom_equal_1
Latex:
\mforall{}prvt:Atom1. \mforall{}pas:ProtocolAction List. Dec(Legal(pas) given prvt)
Date html generated:
2015_07_23-PM-00_14_12
Last ObjectModification:
2015_01_29-AM-07_52_16
Home
Index