| COM | zeno_com | This theory formalizes famous Zeno paradox |
| COM | zeno_author | Pavel Naumov |
| COM | zeno_date | January - February 1996 |
| COM | zeno_local | ~pavel/Nuprl/zeno.thy |
| COM | zeno_web | http://www.cs.cornell.edu/Info/People/pavel/Nuprl/lib/zeno |
| COM | zeno_req | Requires only Nuprl4.2 standard libraries |
| COM | zeno_end_com | ---------------------------------- |
| THM | phole_aux |  n:{1...}. f: (n + 1)   n.
 i:(n + 1). j:{(i + 1)..(n + 1) }. f i = f j |
| THM | phole_aux_ez | n:{1...}. f:(n + 1) n.
i:(n + 1). j:{(i + 1)..(n + 1)}. f i = f j |
| DISP | signature_df | Signature{<i:level>}(<E:E:*><T:T:*><L:L:*>)== Signature(<E><T><L>)
Signature(<E:E:*><T:T:*><L:L:*>)== Signature(<E><T><L>) |
| ABS | signature | Signature(E;T;L) ==
e_rel:(E E  )
 t_rel:(T T )
l_rel:(L L )
inst_e:(E )
time:(E T)
d:(T L)
t0:T
t1:T
def_t:(T )
(L ) |
| THM | signature_wf | E,T,L: . Signature(E;T;L)  ' |
| DISP | sign_e_rel_df | <s:sign:E>.e_rel== <
< == < |
| ABS | sign_e_rel | < == s.1 |
| THM | sign_e_rel_wf | E,T,L:. s:Signature(E;T;L). < E E |
| DISP | sign_t_rel_df | <s:sign:E>.t_rel== <
<== < |
| ABS | sign_t_rel | < == s.2.1 |
| THM | sign_t_rel_wf | E,T,L:. s:Signature(E;T;L). < T T |
| DISP | sign_l_rel_df | <s:sign:E>.l_rel== <
<== < |
| ABS | sign_l_rel | < == s.2.2.1 |
| THM | sign_l_rel_wf | E,T,L:. s:Signature(E;T;L). < L L |
| DISP | sign_inst_e_df | <s:sign:E>.inst_e== I
I== I |
| ABS | sign_inst_e | I == s.2.2.2.1 |
| THM | sign_inst_e_wf | E,T,L:. s:Signature(E;T;L). I E |
| DISP | sign_time_df | <s:sign:E>.time== time
time== time |
| ABS | sign_time | time == s.2.2.2.2.1 |
| THM | sign_time_wf | E,T,L:. s:Signature(E;T;L). time E T |
| DISP | sign_d_df | <s:sign:E>.d== <s>.d |
| ABS | sign_d | s.d == s.2.2.2.2.2.1 |
| THM | sign_d_wf | E,T,L:. s:Signature(E;T;L). s.d T L |
| DISP | sign_t0_df | <s:sign:E>.t0== t0
t0== t0 |
| ABS | sign_t0 | t0 == s.2.2.2.2.2.2.1 |
| THM | sign_t0_wf | E,T,L:. s:Signature(E;T;L). t0 T |
| DISP | sign_t1_df | <s:sign:E>.t1== <s>.t1 |
| ABS | sign_t1 | s.t1 == s.2.2.2.2.2.2.2.1 |
| THM | sign_t1_wf | E,T,L:. s:Signature(E;T;L). s.t1 T |
| DISP | sign_def_t_df | <s:sign:E>.def_t== Def
Def== Def |
| ABS | sign_def_t | Def == s.2.2.2.2.2.2.2.2.1 |
| THM | sign_def_t_wf | E,T,L:. s:Signature(E;T;L). Def T |
| DISP | sign_def_l_df | <s:sign:E>.def_l== Def
Def== Def |
| ABS | sign_def_l | Def == s.2.2.2.2.2.2.2.2.2 |
| THM | sign_def_l_wf | E,T,L:. s:Signature(E;T;L). Def L |
| ML | create_signature | Class Declaration for: s Signature(E;T;L)
Long Name: signature
Short Name: sign
Parameters:
E :
T :
L :
Fields:
(< ) e_rel : E E
(<) t_rel : T T
(sign_x_rel(s)) l_rel : L L
(I) inst_e : E
(time) time : E T
(s.d) d : T L
(t0) t0 : T
(s.t1) t1 : T
(Def) def_t : T
(Def) def_l : L
Universe: ' |
| DISP | sign_t_ref_rel_df | sign_t_ref_rel(<T:T:*><s:s:*>)== 
== |
| ABS | sign_t_ref_rel | ==  x,y.x < y  x = y |
| THM | sign_t_ref_rel_wf | E,T,X:. S:Signature(E;T;X). T T |
| DISP | sign_l_ref_rel_df | sign_l_ref_rel(<L:L:*><S:S:*>)==
== |
| ABS | sign_l_ref_rel | == x,y.x < y x = y |
| THM | sign_l_ref_rel_wf | E,T,L:. S:Signature(E;T;L). L L |
| COM | zeno_vs_jackson | === stuff that Paul Jackson forgot to put into theory gen_algebra_1 ==
= |
| DISP | ir_connex_df | IrConnex(<T:T:*><x:var>,<y:var>.<R:R:*>)== IrConnex(<T><x>,<y>.<R>) |
| ABS | ir_connex | IrConnex(T;x,y.R[x; y]) == x,y:T. R[x; y] x = y R[x; y] |
| THM | ir_connex_wf | T:. R:T T . IrConnex(T;x,y.R[x;y]) |
| DISP | ir_order_df | IrOrder(<T:T:*><x:var>,<y:var>.<R:R:*>)== IrOrder(<T><x>,<y>.<R>) |
| ABS | ir_order | IrOrder(T;x,y.R[x; y]) ==
Irrefl(T;x,y.R[x; y])  Trans(T;x,y.R[x; y]) |
| THM | ir_order_wf | T:. R:T T . IrOrder(T;x,y.R[x;y]) |
| DISP | ir_linorder_df | IrLinorder(<T:T:*><x:var>,<y:var>.<R:R:*>)
== IrLinorder(<T><x>,<y>.<R>) |
| ABS | ir_linorder | IrLinorder(T;x,y.R[x; y]) ==
IrConnex(T;x,y.R[x; y]) IrOrder(T;x,y.R[x; y]) |
| THM | ir_linorder_wf | T:. R:T T . IrLinorder(T;x,y.R[x;y]) |
| COM | back2zeno | === now back to zeno === |
| DISP | run_df | Run(<E:E:*><T:T:*><L:L:*><S:S:*>)== Run(<E><T><L><S>) |
| ABS | run | Run(E;T;L;S) ==
Order(E;e,f.e < f)
IrLinorder(T;t,u.t < u)
IrLinorder(L;x,y.x < y)
t0 < S.t1
(r,u:T. t0 r r < u u S.t1   (S.d r) < (S.d u))
(e,f:E. I e I f (e < f  (time e) < (time f)))
(e:E. n:. w:{f:E| f < e} n. Inj({f:E| f < e} ;n;w))
Def t0
(r:T. t0 r r S.t1 Def r Def (S.d r)) |
| THM | run_wf | E,T,X:. S:Signature(E;T;X). Run(E;T;X;S) |
| DISP | concurrent_df | concurrent{<i:level>}(<E:E:*><T:T:*><L:L:*><S1:S1:*><S2:S2:*>)
== <S1> || <S2>
<S1:S1:*> || <S2:S2:*>== <S1> || <S2> |
| ABS | concurrent | S1 || S2 ==
< = <
< = <
< = <
I = I
time = time
Def = Def
Def = Def |
| THM | concurrent_wf | E,T,L:. S1,S2:Signature(E;T;L). S1 || S2 ' |
| DISP | race_df | race{<i:level>}(<E:E:*><T:T:*><L:L:*><Ach:Ach:*><Tor:Tor:*>)
== <Ach>  <Tor>
<Ach:Ach:*> <Tor:Tor:*>== <Ach> <Tor> |
| ABS | race | Ach Tor ==
Ach || Tor
t0 = t0
(Tor.t1 < Ach.t1
(t:T
(t0 < t
t Ach.t1
Ach.d t = Tor.d t
(s:T. t0 s s < t (Ach.d s) < (Tor.d s)))
Def t)) |
| THM | race_wf | E,T,X:. Ach,Tor:Signature(E;T;X). Ach Tor ' |
| DISP | ivp_df | IVP(<T:T:*><L:L:*><S:S:*>)== IVP(<S>)
IVP(<S:S:*>)== IVP(<S>) |
| ABS | ivp | IVP(S) ==
b,e:T. a:L.
t0 b
b < e
e S.t1
(S.d b) < a
a < (S.d e)
Def b
Def a
Def e
(t:T. b < t t < e S.d t = a Def t) |
| THM | ivp_wf | E,T,L:. S:Signature(E;T;L). IVP(S) |
| THM | successor | E,T,L:. Ach,Tor:Signature(E;T;L). u,w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 u
u < w
(w Ach.t1 w Tor.t1)
(Ach.d u) < (Tor.d u)
Def u
Def w
(v:T. u < v v < w Def v) |
| THM | successor_ez | E,T,L:. Ach,Tor:Signature(E;T;L). u,w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 u
u < w
(w Ach.t1 w Tor.t1)
(Ach.d u) < (Tor.d u)
Def u
Def w
(v:T. u < v v < w Def v) |
| THM | sequence | E,T,L:. Ach,Tor:Signature(E;T;L). w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 < w
(w Ach.t1 w Tor.t1)
(s:T. t0 s s < w (Ach.d s) < (Tor.d s))
Def w
(n:
v:n T
t0 = v 0
(i:(n - 1). (v i) < (v (i + 1)))
(i:n. (v i) < w Def (v i) t0 (v i))) |
| THM | sequence_ez | E,T,L:. Ach,Tor:Signature(E;T;L). w:T.
Run(E;T;L;Ach)
Run(E;T;L;Tor)
Ach Tor
IVP(Ach)
Ach.d w = Tor.d w
t0 < w
(w Ach.t1 w Tor.t1)
(s:T. t0 s s < w (Ach.d s) < (Tor.d s))
Def w
(n:
v:n T
t0 = v 0
(i:(n - 1). (v i) < (v (i + 1)))
(i:n. (v i) < w Def (v i) t0 (v i))) |
| THM | mult_trans | T:. R:T T . n:{2...}. v:n T.
Trans(T;x,y.x R y)
(i:(n - 1). (v i) R (v (i + 1)))
(v 0) R (v (n - 1)) |
| THM | mult_trans_ez | T:. R:T T . n:{2...}. v:n T.
Trans(T;x,y.x R y)
(i:(n - 1). (v i) R (v (i + 1)))
(v 0) R (v (n - 1)) |
| DISP | tep_df | TEP(<E:E:*><T:T:*><S:S:*>)== TEP
TEP== TEP |
| ABS | tep | TEP == t:T. e:E. Def t I e t = time e |
| THM | tep_wf | E,T,L:. S:Signature(E;T;L). TEP |
| THM | sign_t_ref_rel_trans | E,T,L:. S:Signature(E;T;L). u,v,w:T.
Run(E;T;L;S) u v v w u w |
| THM | sign_t_ref_rel_trans_ez | E,T,L:. S:Signature(E;T;L). u,v,w:T.
Run(E;T;L;S) u v v w u w |
| THM | paradox | E,T,L:. Ach,Tor:Signature(E;T;L).
(Run(E;T;L;Ach) Run(E;T;L;Tor))
Ach Tor
Ach.t1 Tor.t1
IVP(Ach)
 TEP |
| THM | paradox_ez | E,T,L:. Ach,Tor:Signature(E;T;L).
(Run(E;T;L;Ach) Run(E;T;L;Tor))
Ach Tor
Ach.t1 Tor.t1
IVP(Ach)
TEP |