40 "wellfounded_on(M,A,r) == |
40 "wellfounded_on(M,A,r) == |
41 \<forall>x[M]. ~ empty(M,x) --> subset(M,x,A) |
41 \<forall>x[M]. ~ empty(M,x) --> subset(M,x,A) |
42 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
42 --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & <z,y> \<in> r))" |
43 |
43 |
44 wellordered :: "[i=>o,i,i]=>o" |
44 wellordered :: "[i=>o,i,i]=>o" |
45 --{*every non-empty subset of @{text A} has an @{text r}-minimal element*} |
45 --{*linear and wellfounded on @{text A}*} |
46 "wellordered(M,A,r) == |
46 "wellordered(M,A,r) == |
47 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
47 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
48 |
48 |
49 |
49 |
50 subsubsection {*Trivial absoluteness proofs*} |
50 subsubsection {*Trivial absoluteness proofs*} |