List of theorems referencing the symbol ARG1_BEF_ARG2
(396) Theorem well_founded_set.0: ((X in s) & (Y in s)) •imp ((not(arg1_bef_arg2(X,Y) & arg1_bef_arg2(Y,X))) & (not arg1_bef_arg2(X,X)))
(398) Theorem well_founded_set.0a: ((T •incin s) & (T /= 0)) •imp ((Minrel_thryvar(T) in T) & (FORALL y in T | (not arg1_bef_arg2(y,Minrel_thryvar(T)))))
(399) Theorem well_founded_set.0b: [Monotonicity of Minrel_thryvar] ((R •incin s) & (T •incin R) & (T /= 0)) •imp (not(arg1_bef_arg2(Minrel_thryvar(T),Minrel_thryvar(R))))
(402) Theorem well_founded_set.1: (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)))))
(405) Theorem well_founded_set.5: [Ordinal enumeration is monotone on ordinals] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(410) Theorem well_ordered_set.0: ((X in s) & (Y in s)) •imp (arg1_bef_arg2(X,Y) or arg1_bef_arg2(Y,X) or (X = Y))
(411) Theorem well_ordered_set.0a: ((T •incin s) & (T /= 0)) •imp (EXISTS x in T | (FORALL y in T | (not arg1_bef_arg2(y,x))))
(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)
(412+) Theorem well_ordered_set.10: ((X in s) & (Y in s)) •imp ((arg1_bef_arg2(X,Y) •imp (not arg1_bef_arg2(Y,X))) & (not arg1_bef_arg2(X,X)))
(413) Theorem well_ordered_set.1: (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)))))
(416) Theorem well_ordered_set.5a: (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(422) Theorem well_ordered_set.5: [Any well-ordering is isomorphic to an ordinal enumeration] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s)) •imp (arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V)) •eq (U in V))
(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})))
(505+) Theorem fin_well_founded.1: ((V •incin s) & (V /= 0)) •imp (EXISTS m in V | (FORALL y in V | not(arg1_bef_arg2(y,m))))
(528) Theorem linear_order_7: (({X,Y} •incin s0) & (arg1_bef_arg2(X,Y) or (X = Y))) •imp ((smaller_thryvar(X,Y) = X) & (smaller_thryvar(Y,X) = X))
(536) Theorem linear_order_15: ({X,Y} •incin s0) •imp ((smaller_thryvar(X,Y) = X) •eq (arg1_bef_arg2(X,Y) or (X = Y)))
(539) Theorem linear_order_18: (Finite(T) & (X in T) & (T •incin s0)) •imp ((max_thryvar(T) in T) & ((X = max_thryvar(T)) or (arg1_bef_arg2(X,max_thryvar(T)))))