{ 
[V:Type]. [eq:EqDecider(V)]. [A:Id List]. [t:
].
([f:V List 
V]
[v,w:V]. [s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))^*) s'))
supposing vs:V List. v:V.
((||vs|| = ((2 * t) + 1))
((t + 1) 
||filter(
x.(eqof(eq) x v);vs)||)
((f vs) = v))) supposing
((||A|| = ((3 * t) + 1)) and
no_repeats(Id;A)) }
{ Proof }
Definitions occuring in Statement :
three-cs-decided: three-cs-decided(V;A;t;f;s;v),
three-consensus-ts: three-consensus-ts(V;A;t;f),
Id: Id,
length: ||as||,
nat_plus: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
infix_ap: x f y,
le: A B,
all: x:A. B[x],
implies: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: 
,
universe: Type,
equal: s = t,
no_repeats: no_repeats(T;l),
filter: filter(P;l),
rel_star: R^*,
eqof: eqof(d),
deq: EqDecider(T),
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts)
Definitions :
so_apply: x[s],
guard: {T},
axiom: Ax,
tag-by: z
T,
rev_implies: P 
Q,
or: P 
Q,
iff: P Q,
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
isect2: T1 
T2,
b-union: A 
B,
union: left + right,
true: True,
fpf-cap: f(x)?z,
spread: spread def,
pi1: fst(t),
intensional-universe: IType,
so_lambda: 
x.t[x],
int_nzero: 
,
archive-condition: archive-condition(V;A;t;f;n;v;L),
iseg: l1 l2,
l_all: (x
L.P[x]),
exists: 
x:A. B[x],
strong-subtype: strong-subtype(A;B),
product: x:A B[x],
and: P 
Q,
uiff: uiff(P;Q),
fpf: a:A fp-> B[a],
ge: i 
j ,
consensus-rcv: consensus-rcv(V;A),
l_member: (x l),
three-cs-decided: three-cs-decided(V;A;t;f;s;v),
ts-rel: ts-rel(ts),
rel_star: R^*,
infix_ap: x f y,
void: Void,
real: 
,
rationals: 
,
subtype: S 
T,
nat: ,
transition-system: transition-system{i:l},
ts-type: ts-type(ts),
subtype_rel: A r B,
three-consensus-ts: three-consensus-ts(V;A;t;f),
ts-reachable: ts-reachable(ts),
top: Top,
eqof: eqof(d),
apply: f a,
lambda: x.A[x],
filter: filter(P;l),
le: A B,
pair: <a, b>,
bool: 
,
less_than: a < b,
natural_number: $n,
multiply: n * m,
add: n + m,
length: ||as||,
limited-type: LimitedType,
false: False,
implies: P Q,
not: 
A,
int: ,
prop: 
,
no_repeats: no_repeats(T;l),
uimplies: b supposing a,
nat_plus: ,
set: {x:A| B[x]} ,
assert: 
b,
all: x:A. B[x],
function: x:A B[x],
isect: x:A. B[x],
uall: [x:A]. B[x],
list: type List,
Id: Id,
universe: Type,
member: t T,
deq: EqDecider(T),
equal: s = t,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
cand: A c B,
three-intersection: three-intersection(A;W),
ts-stable-rel: ts-stable-rel(ts;x,y.R[x; y]),
decide_bfalse: decide_bfalse{decide_bfalse_compseq_tag_def:o}(v11.g[v11]; v21.f[v21]),
sq_type: SQType(T),
sqequal: s ~ t,
id-deq: IdDeq,
list_ind: list_ind def,
grp_car: |g|,
cons: [car / cdr],
cs-rcv-vote: Vote[a;i;v],
rel_implies: R1 => R2,
append: as @ bs,
trans: Trans(T;x,y.E[x; y]),
nil: [],
refl: Refl(T;x,y.E[x; y]),
so_lambda: x y.t[x; y],
IdLnk: IdLnk,
Knd: Knd,
MaName: MaName,
l_disjoint: l_disjoint(T;l1;l2),
consensus-state3: consensus-state3(T),
cs-not-completed: in state s, a has not completed inning i,
cs-archived: by state s, a archived v in inning i,
cs-passed: by state s, a passed inning i without archiving a value,
cs-inning-committed: in state s, inning i has committed v,
cs-inning-committable: in state s, inning i could commit v ,
cs-archive-blocked: in state s, ws' blocks ws from archiving v in inning i,
cs-precondition: state s may consider v in inning i,
decidable: Dec(P),
atom: Atom,
atom: Atom$n,
tl: tl(l),
hd: hd(l),
two-intersection: two-intersection(A;W),
it: 
,
subtract: n - m,
minus: -n,
votes-from-inning: votes-from-inning(i;L),
values-for-distinct: values-for-distinct(eq;L),
select: l[i],
int_seg: {i..j},
lelt: i j < k,
divides: b | a,
assoced: a ~ b,
set_leq: a b,
set_lt: a <p b,
grp_lt: a < b,
l_contains: A B,
inject: Inj(A;B;f),
reducible: reducible(a),
prime: prime(a),
squash: 
T,
l_exists: (xL. P[x]),
fun-connected: y is f*(x),
qle: r s,
qless: r < s,
q-rel: q-rel(r;x),
i-finite: i-finite(I),
i-closed: i-closed(I),
p-outcome: Outcome,
fset-member: a s,
f-subset: xs ys,
fset-closed: (s closed under fs),
proper-iseg: L1 < L2,
compat: l1 || l2,
eq_knd: a = b,
fpf-dom: x dom(f),
ts-init: ts-init(ts),
biject: Bij(A;B;f),
equipollent: A ~ B,
bfalse: ff,
null: null(as),
quotient: x,y:A//B[x; y],
set_car: |p|,
rng_car: |r|,
unit: Unit,
dstype: dstype(TypeNames; d; a),
string: Error :string
Lemmas :
iseg_length,
iseg_same_length,
proper-iseg-length,
decidable__equal_set,
equipollent-subtract2,
equipollent-length,
decidable_wf,
decidable__equal_int_seg,
bool_subtype_base,
bool_wf,
not_assert_elim,
inject_wf,
length-filter-lower-bound,
equipollent_wf,
biject_wf,
int_seg_properties,
deq_property,
archive-condition-one-one,
archive-condition-innings,
compat-iseg-cases,
proper-iseg_wf,
common_iseg_compat,
decidable__lt,
int_seg_wf,
select_wf,
three-cs-archive-condition,
cons_member,
false_wf,
ge_wf,
nat_ind_tp,
three-intersection-two-intersection,
iseg_append,
list_subtype_base,
union_subtype_base,
atom2_subtype_base,
product_subtype_base,
set_subtype_base,
int_subtype_base,
top_wf,
decidable__equal_Id,
ts-transitive-stable,
refl_wf,
iseg_weakening,
trans_wf,
rel_implies_wf,
not_wf,
nat_wf,
cs-rcv-vote_wf,
append_wf,
assert_wf,
exists_functionality_wrt_iff,
and_functionality_wrt_iff,
iff_wf,
rev_implies_wf,
all_functionality_wrt_iff,
implies_functionality_wrt_iff,
iff_weakening_uiff,
not_functionality_wrt_uiff,
assert-eq-id,
subtype_base_sq,
nat_properties,
l_all_wf,
iseg_transitivity,
three-intersecting-wait-set-exists,
consensus-rcv_wf,
three-cs-decided_wf,
le_wf,
nat_plus_properties,
three-consensus-ts_wf,
ts-rel_wf,
ts-type_wf,
rel_star_wf,
subtype_rel_wf,
ts-reachable_wf,
nat_plus_inc,
eqof_wf,
filter_wf,
length_wf1,
Id_wf,
no_repeats_wf,
nat_plus_wf,
deq_wf,
l_member_wf,
member_wf,
length_wf_nat,
archive-condition_wf,
iseg_wf,
l_all_wf2,
intensional-universe_wf,
uiff_inversion
\mforall{}[V:Type]. \mforall{}[eq:EqDecider(V)]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}].
(\mforall{}[f:V List {}\mrightarrow{} V]
\mforall{}[v,w:V]. \mforall{}[s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s'))
supposing \mforall{}vs:V List. \mforall{}v:V.
((||vs|| = ((2 * t) + 1))
{}\mRightarrow{} ((t + 1) \mleq{} ||filter(\mlambda{}x.(eqof(eq) x v);vs)||)
{}\mRightarrow{} ((f vs) = v))) supposing
((||A|| = ((3 * t) + 1)) and
no\_repeats(Id;A))
Date html generated:
2011_08_16-AM-10_17_51
Last ObjectModification:
2011_06_18-AM-09_07_06
Home
Index