List of theorems referencing the symbol NEXT

(54) Theorem 32: [Successor ordinal] Ord(S) •imp Ord(next(S))
(58) Theorem 36: [Membership in the successor of an ordinal s] Ord(S) •imp ((T in next(S)) •eq ((T •incin S) & Ord(T)))
(59) Theorem 37: [Membership of s in an ordinal t implies inclusion of next(s) in t] (Ord(T) & (S in T)) •imp (next(S) •incin T)
(236) Theorem 195: [Finiteness of successor set] Finite(S) •imp Finite(next(S))
(251) Theorem 205: [The successor of an integer is an integer] (I in Za) •imp (Card(next(I)) & (next(I) in Za))
(348) Theorem 301: [The successor integer as a sum] (N •PLUS 1) = #next(N)
(349) Theorem 302: [The successor integer as a sum, 2] (N in Za) •imp ((next(N) in Za) & ((N •PLUS 1) = next(N)))
(359) Theorem 312: ((J in Za - X) & (FORALL i | (next(i) in X) •imp (i in X))) •imp ({h in Za | (h notin J) & (h in X)} = 0)
(360) Theorem 313: ((X •incin Za) & (FORALL i | (next(i) in X) •imp (i in X))) •eq (X in next(Za))
(361) Theorem 314: (({X,Y} •incin next(Za)) & (#X in next(Y))) •imp (((X = Y) & (Y = Za)) or (X in (next(Y) * Za)))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(387) Theorem subseq.3: Svm(g) & (g •incin (domain(f) •PROD range(f))) & (domain(g) in (next(Za) * next(domain(f))))
(389) Theorem 334: ((F in Fin_seqs(S)) & (G in Subseqs(F))) •imp ((G in Fin_seqs(S)) & (domain(G) in next(domain(F))))
(391) Theorem 336: ((F in Fin_seqs(S)) & (M in Za)) •imp ((shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) in next(domain(F))))
(408) Theorem well_founded_set.8: (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o})))
(409) Theorem well_founded_set.9: (ord_thryvar in next(#pow(s))) & Ord(ord_thryvar) & (s = {ordenm_thryvar(x): x in ord_thryvar}) & (FORALL x in ord_thryvar | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in ord_thryvar})
(412) Theorem well_ordered_set.100: (FORALL x,y | ((x in s) & (y in s)) •imp ((not (arg1_bef_arg2(x,y) & arg1_bef_arg2(y,x))) & (not arg1_bef_arg2(x,x)))) & (FORALL x | (not(s •incin {ordenm_thryvar(y): y in x})) •imp ((ordenm_thryvar(x) in (s - {ordenm_thryvar(y): y in x})) & (FORALL y in (s - {ordenm_thryvar(y): y in x}) | not(arg1_bef_arg2(y,ordenm_thryvar(x)))))) & (FORALL x | (s •incin {ordenm_thryvar(y): y in x}) •eq (ordenm_thryvar(x) = s)) & (FORALL x | (ordenm_thryvar(x) /= s) •imp (ordenm_thryvar(x) in s)) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & arg1_bef_arg2(ordenm_thryvar(u),ordenm_thryvar(v))) •imp (u in v)) & (FORALL v | {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(v))} •incin {ordenm_thryvar(x): x in v}) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & (ordenm_thryvar(v) /= s) & (u /= v)) •imp (ordenm_thryvar(u) /= ordenm_thryvar(v))) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o}))) & (FORALL x | ordenm_thryvar(x) = Minrel_thryvar(s - {ordenm_thryvar(y): y in x})) & (FORALL t | Minrel_thryvar(t) = if (t •incin s) & (t /= 0) then arb({m: m in t | (FORALL y in t | (not arg1_bef_arg2(y,m)))}) else s end if)
(498+) Theorem confinedIncrSeq2: [position of first repetition in confined increasing sequence] (m_thryvar in Za) & (e(next(m_thryvar)) = e(m_thryvar)) & ((m_thryvar * {i in Za | e(next(i)) •incin e(i)}) = 0)
(499) Theorem wellfounded_recursive_fcn.100: (FORALL u, v | (Ord(u) & Ord(v) & (orden(u) /= s) & arg1_bef_arg2(orden(u),orden(v))) •imp (u in v)) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(503) Theorem wellfounded_recursive_fcn.4: (FORALL x, t | (x in s) •imp (rk_thryvar(x,t) = Un({next(rk_thryvar(y,t)): y in s | arg1_bef_arg2(y,x) & ([y,x] in t)})))
(529) Theorem linear_order_8: (X in next(s0)) •imp (smaller_thryvar(X,s0) = X)
(531) Theorem linear_order_10: ((X in next(s0)) & (Y in next(s0))) •imp (smaller_thryvar(X,Y) in next(s0))
(532) Theorem linear_order_11: (s0 in next(s0)) & (FORALL x,y,z | ((x in next(s0)) & (y in next(s0)) & (z in next(s0))) •imp (smaller_thryvar(x,smaller_thryvar(y,z)) = smaller_thryvar(smaller_thryvar(x,y),z))) & (FORALL x,y | ((x in next(s0)) & (y in next(s0))) •imp (smaller_thryvar(x,y) = smaller_thryvar(y,x)))
(533) Theorem linear_order_12: (FORALL f | (Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) in next(s0))) & (FORALL x | (cdr(x) in next(s0)) •imp (min_over_thryvar({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f •ON (domain(f) * t)),min_over_thryvar(f •ON (domain(f) - t))))) & (FORALL c,f | ((c in f) & Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f - {c}),cdr(c))))
(541) Theorem linear_order_20: (FORALL x, y | larger_thryvar(x,y) = if ((x notin s0) & (y notin s0)) then s0 elseif (x notin s0) then y elseif (y notin s0) then x elseif arg1_aft_arg2(x,y) then x else y end if) & (FORALL x, y | larger_thryvar(x,y) = larger_thryvar(y,x)) & (FORALL x, y | ({x,y} •incin s0) •imp (larger_thryvar(x,y) in {x,y})) & (FORALL x | (x in next(s0)) •imp (larger_thryvar(x,s0) = x)) & (FORALL x, y, z | larger_thryvar(x,larger_thryvar(y,z)) = larger_thryvar(larger_thryvar(x,y),z)) & (FORALL x, y | ((x in next(s0)) & (y in next(s0))) •imp (larger_thryvar(x,y) in next(s0))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin s0) & Finite(f)) •imp (((p in f) •imp (max_over_thryvar({p}) = (f~[car(p)]))) & (max_over_thryvar(f) = larger_thryvar(max_over_thryvar(f •ON (domain(f) * a)),max_over_thryvar(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin s0) & Finite(f) & (f /= 0)) •imp (max_over_thryvar(f) in range(f))) & (FORALL x, y | ({x,y} •incin s0) •imp ((larger_thryvar(x,y) = x) •eq (arg1_aft_arg2(x,y) or (x = y)))) & (FORALL t | lbs_thryvar(t) = {x in s0 | (FORALL y in (t * s0) | larger_thryvar(y,x) = y)}) & (FORALL t | min_thryvar(t) = arb({s0} + (t * lbs_thryvar(t)))) & (FORALL t | glb_thryvar(t) = arb({s0} + {x in lbs_thryvar(t) | lbs_thryvar(t) •incin lbs_thryvar({x})})) & (lbs_thryvar(0) = s0) & (min_thryvar(0) = s0) & (FORALL t | (lbs_thryvar(t) •incin s0) & (lbs_thryvar(t) = lbs_thryvar(t * s0)) & (min_thryvar(t) = min_thryvar(t * s0))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin s0)) •imp ((min_thryvar(t) in t) & ((x = min_thryvar(t)) or (arg1_aft_arg2(x,min_thryvar(t))))))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))