From 7abc957b9e553577ce0fa0eae8f5ce3f4c648675 Mon Sep 17 00:00:00 2001 From: Benoit <41090811+benjub@users.noreply.github.com> Date: Sun, 21 Jan 2024 11:57:04 +0100 Subject: [PATCH] Uniformize databases preambles and typgraphic conventions (#3779) --- big-unifier.mm | 648 ++++++++++++++++++++++++---------------------- demo0.mm | 110 +++++--- hol.mm | 4 +- iset.mm | 249 ++++++++++++------ miu.mm | 246 +++++++++--------- nf.mm | 684 ++++++++++++++++++++++++++++++++++++------------- ql.mm | 252 +++++++++--------- set.mm | 118 ++++----- 8 files changed, 1402 insertions(+), 909 deletions(-) diff --git a/big-unifier.mm b/big-unifier.mm index d8d0c395f8..25ab557293 100644 --- a/big-unifier.mm +++ b/big-unifier.mm @@ -1,336 +1,370 @@ -$( big-unifier.mm - Version of 30-Aug-2008 +$( This is the Metamath database big-unifier.mm. $) + +$( Metamath is a formal language and associated computer program for + archiving, verifying, and studying mathematical proofs, created by Norman + Dwight Megill (1950--2021). For more information, visit + https://us.metamath.org and + https://github.com/metamath/set.mm, and feel free to ask questions at + https://groups.google.com/g/metamath. $) + +$( The database big-unifier.mm was created by Norman Megill. This is the version + of 30-Aug-2008. $) + + +$( ! +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Metamath source file big-unifier.mm +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. http://creativecommons.org/publicdomain/zero/1.0/ -Norman Megill - http://metamath.org $) +Norman Megill - http://metamath.org + +$) + $( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + big-unifier.mm: Examples of complicated substitutions in condensed detachment +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# -This file (big-unifier.mm) is a unification and substitution test for -Metamath verifiers, where small input expressions blow up to thousands -of symbols. It is a translation of William McCune's "big-unifier.in" -for the OTTER theorem prover: + This file is a unification and substitution test for Metamath verifiers, + where small input expressions blow up to thousands of symbols. It is a + translation of William McCune's "big-unifier.in" for the OTTER theorem + prover: http://www-unix.mcs.anl.gov/AR/award-2003/big-unifier.in http://www-unix.mcs.anl.gov/AR/award-2003/big-unifier.out Description: "Examples of complicated substitutions in condensed - detachment. These occur in Larry Wos's proofs that XCB is a single - axiom for EC." -$) + detachment. These occur in Larry Wos's proofs that XCB is a + single axiom for EC." +$) - $c wff |- e ( , ) $. - $v x y z w v u v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 $. + $c wff |- e ( , ) $. + $v x y z w v u v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 $. - wx $f wff x $. wy $f wff y $. wz $f wff z $. ww $f wff w $. - wv $f wff v $. wu $f wff u $. wv1 $f wff v1 $. wv2 $f wff v2 $. - wv3 $f wff v3 $. wv4 $f wff v4 $. wv5 $f wff v5 $. wv6 $f wff v6 $. - wv7 $f wff v7 $. wv8 $f wff v8 $. wv9 $f wff v9 $. wv10 $f wff v10 $. + wx $f wff x $. + wy $f wff y $. + wz $f wff z $. + ww $f wff w $. + wv $f wff v $. + wu $f wff u $. + wv1 $f wff v1 $. + wv2 $f wff v2 $. + wv3 $f wff v3 $. + wv4 $f wff v4 $. + wv5 $f wff v5 $. + wv6 $f wff v6 $. + wv7 $f wff v7 $. + wv8 $f wff v8 $. + wv9 $f wff v9 $. + wv10 $f wff v10 $. wv11 $f wff v11 $. - $( The binary connective of the language "EC". $) - wi $a wff e ( x , y ) $. + $( The binary connective of the language "EC". $) + wi $a wff e ( x , y ) $. - ${ - ax-mp.1 $e |- x $. - ax-mp.2 $e |- e ( x , y ) $. - $( The inference rule. $) - ax-mp $a |- y $. - $} + ${ + ax-mp.1 $e |- x $. + ax-mp.2 $e |- e ( x , y ) $. + $( The inference rule. $) + ax-mp $a |- y $. + $} - $( The first axiom. $) - ax-maj $a |- e ( e ( e ( e ( e ( x , e ( y , e ( e ( e ( e ( e ( z , e ( - e ( e ( z , u ) , e ( v , u ) ) , v ) ) , e ( e ( w , e ( e ( e ( w , v6 - ) , e ( v7 , v6 ) ) , v7 ) ) , y ) ) , v8 ) , e ( v9 , v8 ) ) , v9 ) ) ) - , x ) , v10 ) , e ( v11 , v10 ) ) , v11 ) $. + $( The first axiom. $) + ax-maj $a |- e ( e ( e ( e ( e ( x , e ( y , e ( e ( e ( e ( e ( z , e ( + e ( e ( z , u ) , e ( v , u ) ) , v ) ) , e ( e ( w , e ( e ( e ( w , v6 + ) , e ( v7 , v6 ) ) , v7 ) ) , y ) ) , v8 ) , e ( v9 , v8 ) ) , v9 ) ) ) + , x ) , v10 ) , e ( v11 , v10 ) ) , v11 ) $. - $( The second axiom. $) - ax-min $a |- e ( e ( e ( e ( e ( e ( x , e ( e ( y , e ( e ( e ( y , z ) - , e ( u , z ) ) , u ) ) , x ) ) , e ( v , e ( e ( e ( v , w ) , e ( v6 , - w ) ) , v6 ) ) ) , v7 ) , v8 ) , e ( v7 , v8 ) ) , e ( v9 , e ( e ( e ( - v9 , v10 ) , e ( v11 , v10 ) ) , v11 ) ) ) $. + $( The second axiom. $) + ax-min $a |- e ( e ( e ( e ( e ( e ( x , e ( e ( y , e ( e ( e ( y , z ) + , e ( u , z ) ) , u ) ) , x ) ) , e ( v , e ( e ( e ( v , w ) , e ( v6 , + w ) ) , v6 ) ) ) , v7 ) , v8 ) , e ( v7 , v8 ) ) , e ( v9 , e ( e ( e ( + v9 , v10 ) , e ( v11 , v10 ) ) , v11 ) ) ) $. - $( A 3-step proof that applies ~ ax-mp to the two axioms. The proof was - saved in compressed format with "save proof theorem1 /compressed" in - the metamath program. $) - theorem1 $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) - , u ) ) ) , v ) , e ( x , v ) ) $= - ( wi ax-min ax-maj ax-mp ) ABBCFECFFEFFZFZKDFADFFZAFZFJMFFZKNJFFNFZFAO - FFZMPAFFZFPFQPFZFLRFFLNKMJAJNQPLAPGPMKBADCEOARLHI $. + $( A three-step proof that applies ~ ax-mp to the two axioms. The proof was + saved in compressed format with "SAVE PROOF theorem1 / COMPRESSED" in the + Metamath program. $) + theorem1 $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) + , u ) ) ) , v ) , e ( x , v ) ) $= + ( wi ax-min ax-maj ax-mp ) ABBCFECFFEFFZFZKDFADFFZAFZFJMFFZKNJFFNFZFAOFFZMP + AFFZFPFQPFZFLRFFLNKMJAJNQPLAPGPMKBADCEOARLHI $. $( This is the same as ~ theorem1 , except that the proof is saved in - uncompressed format with "save proof theorem1u /normal" in the metamath - program. Note the size difference in the compressed vs. uncompressed + uncompressed format with "SAVE PROOF theorem1u / NORMAL" in the Metamath + program. Note the size difference in the compressed versus uncompressed proofs. $) theorem1u $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) ) - , u ) ) ) , v ) , e ( x , v ) ) $= - wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz - wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi - wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi - wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy - wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi - wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv - wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi - wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi - wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi - wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy - wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi - wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy - wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi - wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy - wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy - wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi - wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi - wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi - wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wv wi wx wv wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv - wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi - wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy - wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz - wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz - wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi - wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy - wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi - wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi - wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi - wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu - wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz - wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu - wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi - wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu - wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi - wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx - wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz - wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy - wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz - wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx - wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi - wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wv wi wx wv wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz - wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi - wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi - wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv - wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy - wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu - wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi - wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi - wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy - wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wi wi wi wi ax-min wx wy wy wz wi wu wz wi wi wu wi wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy - wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx - wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi - wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu - wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wv wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wy wx wv wz wu wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi - wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi - wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz - wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wx wx wy wy wz - wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx - wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi - wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx - wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi - wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi - wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi - wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi - wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi - wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv - wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wx wi wi wx wy - wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv - wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu - wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi - wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy - wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz - wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv - wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy - wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi - wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz - wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu - wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi - wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi - wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi - wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi ax-maj ax-mp - $. + , u ) ) ) , v ) , e ( x , v ) ) $= + wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz + wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi + wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi + wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy + wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi + wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv + wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi + wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi + wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi + wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy + wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi + wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy + wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi + wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy + wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy + wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi + wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi + wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi + wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wv wi wx wv wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv + wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi + wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy + wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz + wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz + wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi + wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy + wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi + wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi + wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi + wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu + wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz + wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu + wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi + wx wi wi wi wi wi wi wx wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu + wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi + wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx + wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz + wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy + wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz + wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx + wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi + wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wv wi wx wv wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz + wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi + wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi + wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv + wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy + wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu + wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi + wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi + wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy + wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wi wi wi wi ax-min wx wy wy wz wi wu wz wi wi wu wi wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy + wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx + wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wx wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi + wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu + wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wv wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wy wx wv wz wu wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi + wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi + wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz + wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wx wx wy wy wz + wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx + wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi + wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx + wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi + wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi + wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi + wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi + wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi + wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu wi wi wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv + wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi wi wx wi wi wx wy + wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv + wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu + wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi + wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy + wy wz wi wu wz wi wi wu wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz + wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv + wi wi wx wi wi wi wi wi wx wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy + wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi + wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi wx wy wy wz wi wu wz + wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wy wy wz wi wu wz wi wi wu + wi wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi + wi wu wi wi wi wv wi wx wv wi wi wx wi wi wy wy wz wi wu wz wi wi wu wi wi + wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi wx wi wi wi wi wi + wi wi wx wy wy wz wi wu wz wi wi wu wi wi wi wv wi wx wv wi wi ax-maj ax-mp + $. -$( + $( -This comment holds a simple typesetting definition file so that HTML -pages can be created with "show statement theorem1/html" in the -metamath program. + This comment holds a simple typesetting definition file so that HTML pages + can be created with "show statement theorem1/html" in the Metamath program. -$t -htmldef "(" as " ( "; -htmldef ")" as " ) "; -htmldef "e" as " e "; -htmldef "wff" as " wff "; -htmldef "|-" as " |- "; -htmldef "," as " , "; -htmldef "x" as " x "; -htmldef "y" as " y "; -htmldef "z" as " z "; -htmldef "w" as " w "; -htmldef "v" as " v "; -htmldef "u" as " u "; -htmldef "v1" as " v1 "; -htmldef "v2" as " v2 "; -htmldef "v3" as " v3 "; -htmldef "v4" as " v4 "; -htmldef "v5" as " v5 "; -htmldef "v6" as " v6 "; -htmldef "v7" as " v7 "; -htmldef "v8" as " v8 "; -htmldef "v9" as " v9 "; -htmldef "v10" as " v10 "; -htmldef "v11" as " v11 "; -$) + $t + htmldef "(" as " ( "; + htmldef ")" as " ) "; + htmldef "e" as " e "; + htmldef "wff" as " wff "; + htmldef "|-" as " |- "; + htmldef "," as " , "; + htmldef "x" as " x "; + htmldef "y" as " y "; + htmldef "z" as " z "; + htmldef "w" as " w "; + htmldef "v" as " v "; + htmldef "u" as " u "; + htmldef "v1" as " v1 "; + htmldef "v2" as " v2 "; + htmldef "v3" as " v3 "; + htmldef "v4" as " v4 "; + htmldef "v5" as " v5 "; + htmldef "v6" as " v6 "; + htmldef "v7" as " v7 "; + htmldef "v8" as " v8 "; + htmldef "v9" as " v9 "; + htmldef "v10" as " v10 "; + htmldef "v11" as " v11 "; + + $) diff --git a/demo0.mm b/demo0.mm index 270fd807f5..5ea302cb80 100644 --- a/demo0.mm +++ b/demo0.mm @@ -1,50 +1,80 @@ -$( demo0.mm 1-Jan-04 $) +$( This is the Metamath database demo0.mm. $) + +$( Metamath is a formal language and associated computer program for + archiving, verifying, and studying mathematical proofs, created by Norman + Dwight Megill (1950--2021). For more information, visit + https://us.metamath.org and + https://github.com/metamath/set.mm, and feel free to ask questions at + https://groups.google.com/g/metamath. $) + +$( The database demo0.mm was created by Norman Megill. This is the version + of 1-Jan-2004. $) + + +$( ! +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Metamath source file demo0.mm +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# -$( ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. http://creativecommons.org/publicdomain/zero/1.0/ -Norman Megill +Norman Megill - http://metamath.org + +$) + + +$( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + demo0.mm: An introductory formal system example +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + + This file is the introductory formal system example described in Chapter 2 of + the Metamath book. $) +$( Declare the constant symbols we will use. $) + $c 0 + = -> ( ) term wff |- $. + +$( Declare the metavariables we will use. $) + $v t r s P Q $. + +$( Specify properties of the metavariables. $) + tt $f term t $. + tr $f term r $. + ts $f term s $. + wp $f wff P $. + wq $f wff Q $. + +$( Define "term" (part 1 of 2). $) + tze $a term 0 $. + +$( Define "term" (part 2 of 2). $) + tpl $a term ( t + r ) $. + +$( Define "wff" (part 1 of 2). $) + weq $a wff t = r $. + +$( Define "wff" (part 2 of 2). $) + wim $a wff ( P -> Q ) $. + +$( State axiom ~ a1 . $) + a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. + +$( State axiom ~ a2 . $) + a2 $a |- ( t + 0 ) = t $. + + ${ + min $e |- P $. + maj $e |- ( P -> Q ) $. + $( Define the modus ponens inference rule. $) + mp $a |- Q $. + $} -$( This file is the introductory formal system example described - in Chapter 2 of the Meamath book. $) - -$( Declare the constant symbols we will use $) - $c 0 + = -> ( ) term wff |- $. -$( Declare the metavariables we will use $) - $v t r s P Q $. -$( Specify properties of the metavariables $) - tt $f term t $. - tr $f term r $. - ts $f term s $. - wp $f wff P $. - wq $f wff Q $. -$( Define "term" (part 1) $) - tze $a term 0 $. -$( Define "term" (part 2) $) - tpl $a term ( t + r ) $. -$( Define "wff" (part 1) $) - weq $a wff t = r $. -$( Define "wff" (part 2) $) - wim $a wff ( P -> Q ) $. -$( State axiom a1 $) - a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. -$( State axiom a2 $) - a2 $a |- ( t + 0 ) = t $. - ${ - min $e |- P $. - maj $e |- ( P -> Q ) $. -$( Define the modus ponens inference rule $) - mp $a |- Q $. - $} -$( Prove a theorem $) - th1 $p |- t = t $= +$( Prove a theorem. $) + th1 $p |- t = t $= $( Here is its proof: $) - tt tze tpl tt weq tt tt weq tt a2 tt tze tpl - tt weq tt tze tpl tt weq tt tt weq wim tt a2 - tt tze tpl tt tt a1 mp mp - $. + tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt + weq wim tt a2 tt tze tpl tt tt a1 mp mp $. diff --git a/hol.mm b/hol.mm index 172ef8b151..6b0c534722 100644 --- a/hol.mm +++ b/hol.mm @@ -5,14 +5,14 @@ Dwight Megill (1950--2021). For more information, visit https://us.metamath.org and https://github.com/metamath/set.mm, and feel free to ask questions at - https://groups.google.com/group/metamath. $) + https://groups.google.com/g/metamath. $) $( The database hol.mm was created by Mario Carneiro on 7-Oct-2014. $) $( ! #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# - Metamath source file for higher order logic + Metamath source file for higher-order logic #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ diff --git a/iset.mm b/iset.mm index dc35550dce..25b167e2cc 100644 --- a/iset.mm +++ b/iset.mm @@ -5,7 +5,7 @@ Dwight Megill (1950--2021). For more information, visit https://us.metamath.org and https://github.com/metamath/set.mm, and feel free to ask questions at - https://groups.google.com/group/metamath. $) + https://groups.google.com/g/metamath. $) $( New users may want to read https://us.metamath.org/ileuni/conventions.html to understand the label naming conventions used in iset.mm. See also the @@ -80,9 +80,17 @@ Dwight Megill (1950--2021). For more information, visit DAW David A. Wheeler JY Jonathan Yan FZ Fan Zheng + +HTML code for accented names: + BJ Benoît Jubin + GL Gérard Lang + FL Frédéric Liné + $) +$( See "MM> HELP VERIFY MARKUP" for help with modularization tags. $) +$( Begin $[ iset-header.mm $] $) $( ! =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Contents of this header @@ -103,9 +111,9 @@ Dwight Megill (1950--2021). For more information, visit 1. Download the program metamath.exe per the instructions on the Metamath home page (https://us.metamath.org) and put it in the same - directory as this file (set.mm). + directory as this file. 2. In Windows Explorer, double-click on metamath.exe. -3. Type "read set.mm" and press Enter. +3. Type "read iset.mm" and press Enter. 4. Type "help" for a list of help topics, and "help demo" for some command examples. @@ -121,13 +129,24 @@ directory as this file (set.mm). Logic and set theory - see https://us.metamath.org/mpegif/mmset.html#bib Hilbert space - see https://us.metamath.org/mpegif/mmhil.html#ref +A bracketed reference must be preceded by a theorem number, etc. and followed +by a page number. See "MM> HELP WRITE BIBLIOGRAPHY" for details. + =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Metamath syntax summary =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The HELP LANGUAGE command in the Metamath program will give you a quick -overview of Metamath. Syntax summary: +overview of Metamath. The specification is found on pp. 92--95 of the +Metamath book. The following syntax summary is provided for convenience +but may omit some details. + +A Metamath database (set of one or more ASCII source files) is a sequence of +_tokens_, which are normally separated by spaces or line breaks. The only +tokens that are built into the Metamath language are those (two-character +sequences) beginning with $, shown in the following. These tokens are called +_keywords_: $c ... $. - Constant declaration $v ... $. - Variable declaration @@ -150,13 +169,16 @@ directory as this file (set.mm). checking for distinct variable violations. Everything else, including the axioms for logic, is defined in this database file. -Here is some more detail about the syntax. There are two kinds of user-defined -syntax elements, called math symbols (or just symbols) and labels. A symbol -may contain any non-whitespace printable character except "$". A label may -contain only alphanumeric characters and the characters "." (period), "-" -(hyphen), and "_" (underscore). Tokens and labels are case-sensitive. All -labels (except in proofs) must be distinct. A label may not have the same name -as a token (to simplify the coding of certain parsers and translators). +All other tokens are user-defined, and their names are arbitrary. There are +two kinds of user-defined tokens, called math symbols (or just symbols) and +labels. A _symbol_ may contain any non-whitespace printable character except +"$". A _label_ may contain only alphanumeric characters and the characters "." +(period), "-" (hyphen), and "_" (underscore). Symbols and labels are +case-sensitive. All labels (except in proofs) must be distinct. A label may +not have the same name as a symbol (to simplify the coding of certain parsers +and translators). + +Here is some more detail about the syntax: $c $. is a (whitespace-separated) list of distinct symbols that @@ -207,31 +229,32 @@ and math symbol tokens be enclosed in grave accents (` `). This way the LaTeX Metamath program reads the compressed format directly. This format is described in an Appendix of the Metamath book. It is not intended to be read by humans. For viewing proofs you should use the various SHOW PROOF commands -described in the Metamath book (or the on-line HELP). +described in the Metamath book (or the online HELP). -The Metamath program does not normally affect any content of this file (set.mm) -other than proofs, i.e. tokens between "$=" and "$.". All other content is -user-created. Proofs are created or modified with the PROVE command. +The Metamath program does not normally affect any content of this file other +than proofs, i.e., the text between "$=" and "$." (and some rewrapping). All +other content is user-created. Proofs are created or modified with the PROVE +command. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Other notes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -1. It is recommended that you be familiar with chapters 2 and 4 of the -'Metamath' book to understand the Metamath language. Chapters 2, 3 and 5 -explain how to use the program. Chapter 3 gives you an informal overview of -what this source file is all about. Appendix A shows you the standard -mathematical symbols corresponding to some of the ASCII tokens in this file. +1. It is recommended that you be familiar with Chapters 2 and 4 of the +Metamath book to understand the Metamath language. Chapters 2, 3 and 5 explain +how to use the Metamath program. Chapter 3 gives an informal overview of what +this source file is all about. Appendix A gives the standard mathematical +symbols corresponding to some of the ASCII tokens used in this file. The ASCII tokens may seem cryptic at first, even if you are familiar with set theory, but a review of the definition summary in Chapter 3 should quickly enable you to see the correspondence to standard mathematical notation. To easily find the definition of a token, search for the first occurrences of the token surrounded by spaces. Some odd-looking ones include "-." for "not", and -"C_" for "is a subset of." (HELP TEX tells you how to obtain a LaTeX output to -see the real mathematical symbols.) Let me know if you have better suggestions -for naming ASCII tokens. +"C_" for "is a subset of". The Metamath program "MM> HELP TEX" command +explains how to obtain a LaTeX output to see the real mathematical symbols. +Let us know if you have better suggestions for naming ASCII tokens. 2. Logic and set theory provide a foundation for all of mathematics. To learn about them, you should study one or more of the references listed below. The @@ -358,11 +381,45 @@ compressed proof steps and less on the length of the label section (since the $) +$( End $[ iset-header.mm $] $) + + +$( Begin $[ iset-pred.mm $] $) + +$( The following header is the first to appear in the Theorem List contents, + because higher-level headers suppress all previous same-level or + lower-level headers in the same comment area between $a and $p statements. + See "MM> HELP WRITE THEOREM_LIST" for information about headers. $) $( ############################################################################### - FIRST ORDER LOGIC WITH EQUALITY + INTUITIONISTIC FIRST-ORDER LOGIC WITH EQUALITY ############################################################################### + + Logic can be defined as the "study of the principles of correct reasoning" + (Merrilee H. Salmon's 1991 "Informal Reasoning and Informal Logic" in + _Informal Reasoning and Education_ ) or as "a formal system using symbolic + techniques and mathematical methods to establish truth-values" (the Oxford + English Dictionary). + + This section formally defines the logic system we will use. In particular, + it defines symbols for declaring truthful statements, along with rules for + deriving truthful statements from other truthful statements. The system + defined here is intuitionistic first-order logic with equality. + + We begin with a few housekeeping items in pre-logic, and then introduce + propositional calculus (both its axioms and important theorems that can be + derived from them). Propositional calculus deals with general truths about + well-formed formulas (wffs) regardless of how they are constructed. This is + followed by proofs that other axiomatizations of classical propositional + calculus can be derived from the axioms we have chosen to use. + + We then define predicate calculus, which adds additional symbols and rules + useful for discussing objects (beyond simply true or false). In particular, + it introduces the symbols ` = ` ("equals"), ` e. ` ("is a member of"), and ` + A. ` ("for all"). The first two are called "predicates." A predicate + specifies a true or false relationship between its two arguments. + $) @@ -379,12 +436,12 @@ compressed proof steps and less on the length of the label section (since the $( Declare the primitive constant symbols for propositional calculus. $) $c ( $. $( Left parenthesis $) $c ) $. $( Right parenthesis $) - $c -> $. $( Right arrow (read: "implies") $) - $c -. $. $( Right handle (read: "not") $) - $c wff $. $( Well-formed formula symbol (read: "the following symbol - sequence is a wff") $) - $c |- $. $( Turnstile (read: "the following symbol sequence is provable" or - 'a proof exists for") $) + $c -> $. $( Right arrow (read: "implies") $) + $c -. $. $( Right handle (read: "not") $) + $c wff $. $( Well-formed formula symbol (read: "the following symbol + sequence is a wff") $) + $c |- $. $( Turnstile (read: "the following symbol sequence is provable" or + 'a proof exists for") $) $( Define the syntax and logical typecodes, and declare that our grammar is unambiguous (verifiable using the KLR parser, with compositing depth 5). @@ -396,13 +453,11 @@ compressed proof steps and less on the length of the label section (since the unambiguous 'klr 5'; $) - $( Declare typographical constant symbols that are not directly used - in the formalism, but *are* symbols we find useful when - explaining the formalism. It is much easier to consistently use - a single typographical system when generating text. $) + $( Declare typographical constant symbols that are not directly used in the + formalism but are useful to explain it in comments. $) - $c & $. $( Ampersand (read: "and-also") $) - $c => $. $( Big-to (read: "proves") $) + $c & $. $( Ampersand (read: "and"). $) + $c => $. $( Double right arrow (read: "implies"). $) $( wff variable sequence: ph ps ch th ta et ze si rh mu la ka $) $( Introduce some variable names we will use to represent well-formed @@ -521,10 +576,31 @@ The Metamath (Metamath-exe) program Proof Assistant requires proofs to ( ) C $. $} + $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Propositional calculus #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + + Propositional calculus deals with general truths about well-formed formulas + (wffs) regardless of how they are constructed. The simplest propositional + truth is ` ( ph -> ph ) ` , which can be read "if something is true, then it + is true" - rather trivial and obvious, but nonetheless it must be proved from + the axioms (see theorem ~ id ). + + Our system of propositional calculus consists of a few basic axioms and a + unique rule of inference, modus ponens. + + The propositional calculus used here is the intuitionistic propositional + calculus. + + All 194 axioms, definitions, and theorems for propositional calculus in + _Principia Mathematica_ (specifically *1.2 through *5.75) are axioms or + formally proven. See the Bibliographic Cross-References at + ~ http://us.metamath.org/ileuni/mmbiblio.html for a complete + cross-reference from sources used to its formalization in the Intuitionistic + Logic Explorer. + $) @@ -543,6 +619,10 @@ will extend the basic wff definition by including atomic wffs ( ~ weq and ~ wel ). $) wn $a wff -. ph $. + $( Register negation '-.' as a primitive expression (lacking a + definition). $) + $( $j primitive 'wn'; $) + $( If ` ph ` and ` ps ` are wff's, so is ` ( ph -> ps ) ` or " ` ph ` implies ` ps ` ." Part of the recursive definition of a wff. The left-hand wff is called the antecedent, and the right-hand wff is called the consequent. @@ -551,6 +631,10 @@ will extend the basic wff definition by including atomic wffs ( ~ weq and on context. $) wi $a wff ( ph -> ps ) $. + $( Register implication '->' as a primitive expression (lacking a + definition). $) + $( $j primitive 'wi'; $) + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -558,6 +642,28 @@ will extend the basic wff definition by including atomic wffs ( ~ weq and =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) + ${ + $( Minor premise for modus ponens. $) + min $e |- ph $. + $( Major premise for modus ponens. $) + maj $e |- ( ph -> ps ) $. + $( Rule of Modus Ponens. The postulated inference rule of propositional + calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if + ` ph ` is true, and ` ph ` implies ` ps ` , then ` ps ` must also be + true." This rule is sometimes called "detachment", since it detaches + the minor premise from the major premise. "Modus ponens" is short for + "modus ponendo ponens", a Latin phrase that means "the mode that by + affirming affirms" - remark in [Sanford] p. 39. This rule is similar to + the rule of modus tollens ~ mto . + + Note: In some web page displays such as the Statement List, the + symbols " ` & ` " and " ` => ` " informally indicate the relationship + between the hypotheses and the assertion (conclusion), abbreviating the + English words "and" and "implies." They are not part of the formal + language. (Contributed by NM, 30-Sep-1992.) $) + ax-mp $a |- ps $. + $} + $( Axiom _Simp_. Axiom A1 of [Margaris] p. 49. One of the axioms of propositional calculus. This axiom is called _Simp_ or "the principle of simplification" in _Principia Mathematica_ (Theorem *2.02 of @@ -579,44 +685,22 @@ will extend the basic wff definition by including atomic wffs ( ~ weq and (Contributed by NM, 5-Aug-1993.) $) ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $. - $( - Postulate the modus ponens rule of inference. - $) - - ${ - $( Minor premise for modus ponens. $) - min $e |- ph $. - $( Major premise for modus ponens. $) - maj $e |- ( ph -> ps ) $. - $( Rule of Modus Ponens. The postulated inference rule of propositional - calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if - ` ph ` is true, and ` ph ` implies ` ps ` , then ` ps ` must also be - true." This rule is sometimes called "detachment," since it detaches - the minor premise from the major premise. - - Note: In some web page displays such as the Statement List, the symbols - "&" and "=>" informally indicate the relationship between the hypotheses - and the assertion (conclusion), abbreviating the English words "and" and - "implies." They are not part of the formal language. (Contributed by - NM, 5-Aug-1993.) $) - ax-mp $a |- ps $. - $} - $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Logical implication =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - The results in this section are based on implication only, and only use - ~ ax-1 , ~ ax-2 , and ~ ax-mp . - In an implication, the wff before the arrow is called the "antecedent" and - the wff after the arrow is called the "consequent." + The results in this section are based on implication only, and only use + ~ ax-1 , ~ ax-2 , and ~ ax-mp . In an implication, the wff before the arrow + is called the "antecedent" and the wff after the arrow is called the + "consequent". + + We will use the following descriptive terms very loosely: A "closed form" or + "tautology" has no $e hypotheses. An "inference" has one or more $e + hypotheses. A "deduction" is an inference in which the hypotheses and the + conclusion share the same antecedent. - We will use the following descriptive terms very loosely: A "closed form" - or "tautology" has no $e hypotheses. An "inference" has one or more $e - hypotheses. A "deduction" is an inference in which the hypotheses and the - conclusion share the same antecedent. $) ${ @@ -17510,6 +17594,8 @@ existence hypothesis (to prove the "some" in the conclusion). Example ( wa wi spi syl ancri eximii ) ACAHDGACABCABIDEJBCIDFJKLM $. $} +$( End $[ iset-pred.mm $] $) + $( ############################################################################### @@ -141706,7 +141792,6 @@ S C_ ( P ( ball ` D ) T ) ) $= ABXICXQUVCUVAWTXAXBXC $. $} - ${ cnplimccntop.k $e |- K = ( MetOpen ` ( abs o. - ) ) $. cnplimc.j $e |- J = ( K |`t A ) $. @@ -143163,14 +143248,14 @@ S C_ ( P ( ball ` D ) T ) ) $= Conventions =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= - This section describes the conventions we use. However, these conventions - often refer to existing mathematical practices, which are discussed in more - detail in other references. + This section describes the conventions we use. These conventions often refer + to existing mathematical practices, which are discussed in more detail in + other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too - (especially in a treatment such as ours which is built on first order logic + (especially in a treatment such as ours which is built on first-order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic @@ -143198,7 +143283,7 @@ good place to start (and is easy to compare with the Intuitionistic Logic $) ${ - $( Dummy premise for "conventions" $) + $( Dummy premise for ~ conventions . $) conventions.1 $e |- ph $. $( Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (MPE, set.mm). This list of conventions is @@ -143327,7 +143412,7 @@ different should be named differently (we do have a small number of
  • Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: - ~ https://groups.google.com/forum/#!forum/metamath . + ~ https://groups.google.com/g/metamath .
    • @@ -143559,14 +143644,6 @@ Norman Megill (2007) section 1.1.3. Megill then states, "A number of " -> "; althtmldef "->" as " → "; latexdef "->" as " \rightarrow "; -htmldef "&" as - " & "; - althtmldef "&" as " & "; - latexdef "&" as "\mathrel{\&}"; -htmldef "=>" as - " => "; - althtmldef "=>" as " ⇒ "; - latexdef "=>" as " \Rightarrow "; htmldef "-." as " -. "; althtmldef "-." as '¬ '; @@ -143583,6 +143660,14 @@ Norman Megill (2007) section 1.1.3. Megill then states, "A number of /* Without sans-serif, way too big in FF3 */ /* 2-Jan-2016 reverted sans-serif */ latexdef "|-" as "\vdash"; +htmldef "&" as + " & "; + althtmldef "&" as " & "; + latexdef "&" as "\mathrel{\&}"; +htmldef "=>" as + " => "; + althtmldef "=>" as " ⇒ "; + latexdef "=>" as " \Rightarrow "; htmldef "ph" as " ph"; /* althtmldef "ph" as '𝜑'; */ diff --git a/miu.mm b/miu.mm index 40173fdc3b..7eda08b63c 100644 --- a/miu.mm +++ b/miu.mm @@ -1,6 +1,19 @@ -$( miu.mm 20-Oct-2008 $) +$( This is the Metamath database miu.mm. $) + +$( Metamath is a formal language and associated computer program for + archiving, verifying, and studying mathematical proofs, created by Norman + Dwight Megill (1950--2021). For more information, visit + https://us.metamath.org and + https://github.com/metamath/set.mm, and feel free to ask questions at + https://groups.google.com/g/metamath. $) + +$( The database miu.mm was created by Norman Megill. $) -$( + +$( ! +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Metamath source file for Hofstadter's MIU system +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 @@ -10,121 +23,122 @@ $) -$( The MIU-system: A simple formal system $) - -$( Note: This formal system is unusual in that it allows empty wffs. -To work with a proof, you must type SET EMPTY_SUBSTITUTION ON before -using the PROVE command. By default this is OFF in order to reduce the -number of ambiguous unification possibilities that have to be selected -during the construction of a proof. $) $( -Hofstadter's MIU-system is a simple example of a formal -system that illustrates some concepts of Metamath. See -Douglas R. Hofstadter, "G\"{o}del, Escher, Bach: An Eternal -Golden Braid" (Vintage Books, New York, 1979), pp. 33ff. for -a description of the MIU-system. - -The system has 3 constant symbols, M, I, and U. The sole -axiom of the system is MI. There are 4 rules: - Rule I: If you possess a string whose last letter is I, - you can add on a U at the end. - Rule II: Suppose you have Mx. Then you may add Mxx to - your collection. - Rule III: If III occurs in one of the strings in your - collection, you may make a new string with U in place - of III. - Rule IV: If UU occurs inside one of your strings, you - can drop it. - -Note: The following comment applied to an old version of the Metamath -spec that didn't require $f (variable type) hypotheses for variables and -is no longer applicable. The current spec was made stricter primarily -to reduce the likelihood of inconsistent toy axiom systems, effectively -requiring the concept of an "MIU wff" anyway. However, I am keeping the -comment for historical reasons, if only to point out an intrinsic -difference in Rules III and IV that might have relevance to other proof -systems. - - Old comment, obsolete: "Unfortunately, Rules III and IV do not have - unique results: strings could have more than one occurrence of III or - UU. This requires that we introduce the concept of an "MIU well-formed - formula" or wff, which allows us to construct unique symbol sequences to - which Rules III and IV can be applied." - -Under the old Metamath spec, the problem this caused was that without -the construction of specific wffs to substitute for their variables, -Rules III and IV would sometimes not have unique unifications (as -required by the spec) during a proof, making proofs more difficult or -even impossible. +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + The MIU-system: A simple formal system +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + + Note: This formal system is unusual in that it allows empty wffs. To work + with a proof, you must type "MM> SET EMPTY_SUBSTITUTION ON" before using the + PROVE command. By default this is OFF in order to reduce the number of + ambiguous unification possibilities that have to be selected during the + construction of a proof. + + Hofstadter's MIU-system is a simple example of a formal system that + illustrates some concepts of Metamath. See + + Douglas R. Hofstadter, + "G\"{o}del, Escher, Bach: An Eternal Golden Braid" + (Vintage Books, New York, 1979), pp. 33ff. + + for a description of the MIU-system. + + The system has three constant symbols, M, I, and U. The sole axiom of the + system is MI. There are four rules: + Rule I: If you possess a string whose last letter is I, you can add + append a U at the end. + Rule II: Suppose you have Mx. Then you may add Mxx to your collection. + Rule III: If III occurs in one of the strings in your collection, you may + make a new string with U in place of III. + Rule IV: If UU occurs inside one of your strings, you can drop it. + + Note: The following comment applied to an old version of the Metamath spec + that didn't require $f (variable type) hypotheses for variables and is no + longer applicable. The current spec was made stricter primarily to reduce + the likelihood of inconsistent toy axiom systems, effectively requiring the + concept of an "MIU wff" anyway. However, I am keeping the comment for + historical reasons, if only to point out an intrinsic difference in Rules III + and IV that might have relevance to other proof systems. + + Old comment, obsolete: Unfortunately, Rules III and IV do not have unique + results: strings could have more than one occurrence of III or UU. This + requires that we introduce the concept of an "MIU well-formed formula" or + wff, which allows us to construct unique symbol sequences to which Rules III + and IV can be applied. + + Under the old Metamath spec, the problem this caused was that without the + construction of specific wffs to substitute for their variables, Rules III + and IV would sometimes not have unique unifications (as required by the spec) + during a proof, making proofs more difficult or even impossible. + $) -$( First, we declare the constant symbols of the language. -Note that we need two symbols to distinguish the assertion -that a sequence is a wff from the assertion that it is a -theorem; we have arbitrarily chosen "wff" and "|-". $) - $c M I U |- wff $. $( Declare constants $) - -$( Next, we declare some variables. $) - $v x y $. - -$( Throughout our theory, we shall assume that these -variables represent wffs. $) - wx $f wff x $. - wy $f wff y $. - -$( Define MIU-wffs. We allow the empty sequence to be a -wff. $) - - $( The empty sequence is a wff. $) - we $a wff $. - $( "M" after any wff is a wff. $) - wM $a wff x M $. - $( "I" after any wff is a wff. $) - wI $a wff x I $. - $( "U" after any wff is a wff. $) - wU $a wff x U $. - $( If "x" and "y" are wffs, so is "x y". This allows the conclusion of - ` IV ` to be provable as a wff before substitutions into it, for those - parsers requiring it. (Added per suggestion of Mel O'Cat 4-Dec-04.) $) - wxy $a wff x y $. - - $( Assert the axiom. $) - ax $a |- M I $. - - $( Assert the rules. $) - ${ - Ia $e |- x I $. - $( Given any theorem ending with "I", it remains a theorem - if "U" is added after it. (We distinguish the label I_ - from the math symbol I to conform to the 24-Jun-2006 - Metamath spec change.) $) - I_ $a |- x I U $. - $} - - ${ - IIa $e |- M x $. - $( Given any theorem starting with "M", it remains a theorem - if the part after the "M" is added again after it. $) - II $a |- M x x $. - $} - - ${ - IIIa $e |- x I I I y $. - $( Given any theorem with "III" in the middle, it remains a - theorem if the "III" is replace with "U". $) - III $a |- x U y $. - $} - - ${ - IVa $e |- x U U y $. - $( Given any theorem with "UU" in the middle, it remains a - theorem if the "UU" is deleted. $) - IV $a |- x y $. - $} - - $( Now we prove the theorem MUIIU. You may be interested in - comparing this proof with that of Hofstadter (pp. 35 - 36). $) - theorem1 $p |- M U I I U $= - we wM wU wI we wI wU we wU wI wU we wM we wI wU we wM - wI wI wI we wI wI we wI ax II II I_ III II IV $. + $( First, we declare the constant symbols of the language. Note that we need + two symbols to distinguish the assertion that a sequence is a wff from the + assertion that it is a theorem; we have arbitrarily chosen "wff" and + "|-". $) + $c M I U |- wff $. + + $( Next, we declare some variables. $) + $v x y $. + + $( Throughout our theory, we shall assume that these variables represent + wffs. $) + wx $f wff x $. + wy $f wff y $. + + $( Define MIU-wffs. We allow the empty sequence to be a wff. $) + + $( The empty sequence is a wff. $) + we $a wff $. + $( "M" after any wff is a wff. $) + wM $a wff x M $. + $( "I" after any wff is a wff. $) + wI $a wff x I $. + $( "U" after any wff is a wff. $) + wU $a wff x U $. + + $( If "x" and "y" are wffs, so is "x y". This allows the conclusion of Rule + IV to be provable as a wff before substitutions into it, for those parsers + requiring it. (Added per suggestion of Mel O'Cat, 4-Dec-2004.) $) + wxy $a wff x y $. + + $( Assert the axiom. $) + ax $a |- M I $. + + $( Assert the rules. $) + ${ + Ia $e |- x I $. + $( Given any theorem ending with "I", it remains a theorem if "U" is added + after it. (We distinguish the label ~ I_ from the math symbol ` I ` to + conform to the 24-Jun-2006 Metamath spec change.) $) + I_ $a |- x I U $. + $} + + ${ + IIa $e |- M x $. + $( Given any theorem starting with "M", it remains a theorem if the part + after the "M" is added again after it. $) + II $a |- M x x $. + $} + + ${ + IIIa $e |- x I I I y $. + $( Given any theorem with "III" in the middle, it remains a theorem if the + "III" is replaced with "U". $) + III $a |- x U y $. + $} + + ${ + IVa $e |- x U U y $. + $( Given any theorem with "UU" in the middle, it remains a theorem if the + "UU" is deleted. $) + IV $a |- x y $. + $} + + $( Now we prove the theorem MUIIU. You may be interested in comparing this + proof with that of Hofstadter (pp. 35--36). $) + theorem1 $p |- M U I I U $= + we wM wU wI we wI wU we wU wI wU we wM we wI wU we wM wI wI wI we wI wI we + wI ax II II I_ III II IV $. diff --git a/nf.mm b/nf.mm index 18c7ddb69d..e0896f1e50 100644 --- a/nf.mm +++ b/nf.mm @@ -1,21 +1,229 @@ -$( nf.mm - Version of 22-Feb-2021. $) +$( This is the Metamath database nf.mm. $) + +$( Metamath is a formal language and associated computer program for + archiving, verifying, and studying mathematical proofs, created by Norman + Dwight Megill (1950--2021). For more information, visit + https://us.metamath.org and + https://github.com/metamath/set.mm, and feel free to ask questions at + https://groups.google.com/g/metamath. $) + +$( New users may want to read https://us.metamath.org/nfeuni/conventions.html + to understand the label naming conventions used in nf.mm. See also the + Metamath program command "MM> HELP VERIFY MARKUP" for markup conventions. $) + +$( To break this file into smaller modules, in the Metamath program type + "MM> READ nf.mm" followed by "MM> WRITE SOURCE nf.mm / SPLIT". To + recombine, omit "/ SPLIT". $) + +$( The database nf.mm was created by Scott Fenton on 12-Sep-2005 from a fork of + the database set.mm and has been continuously enriched since then (list of + contributors below). $) + + +$( ! +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Metamath source file for New Foundations set theory +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# -$( ~~ PUBLIC DOMAIN ~~ This work is waived of all rights, including copyright, according to the CC0 Public Domain Dedication. http://creativecommons.org/publicdomain/zero/1.0/ -Principal curator: Scott Fenton +Currently active maintainers: See the list in the CONTRIBUTING.md file. + +Contributor list (partial): + +MC Mario Carneiro +SF Scott Fenton +NM Norman Megill + +$) + + +$( See "MM> HELP VERIFY MARKUP" for help with modularization tags. $) +$( Begin $[ nf-header.mm $] $) +$( ! +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Contents of this header +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + +* Quick "How To" +* Bibliography +* Metamath syntax summary +* Other notes + + +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Quick "How To" +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + +How to use this file under Windows 95/98/NT/2K/XP/Vista/7/10: + +1. Download the Metamath program metamath.exe following the instructions on the + Metamath home page (https://us.metamath.org) and put it in the same + directory as this file. +2. In Windows Explorer, double-click on metamath.exe. +3. Type "read nf.mm" and press Enter. +4. Type "help" for a list of help topics, and "help demo" for some + command examples. + + +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Bibliography +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + +Bibliographical references are made by bracketing an identifier in a theorem's +comment, such as [RussellWhitehead]. These refer to HTML tags on the following +web pages: + + Logic and set theory - see https://us.metamath.org/mpeuni/mmset.html#bib + Hilbert space - see https://us.metamath.org/mpeuni/mmhil.html#ref + +A bracketed reference must be preceded by a theorem number, etc. and followed +by a page number. See "MM> HELP WRITE BIBLIOGRAPHY" for details. + + +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= + Metamath syntax summary +=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= -Partly based on the set.mm database, itself dedicated to public domain -by mean of the CC0 Public Domain Dedication. +The HELP LANGUAGE command in the Metamath program will give you a quick +overview of Metamath. The specification is found on pp. 92--95 of the +Metamath book. The following syntax summary is provided for convenience +but may omit some details. + +A Metamath database (set of one or more ASCII source files) is a sequence of +_tokens_, which are normally separated by spaces or line breaks. The only +tokens that are built into the Metamath language are those (two-character +sequences) beginning with $, shown in the following. These tokens are called +_keywords_: + + $c ... $. - Constant declaration + $v ... $. - Variable declaration + $d ... $. - Disjoint (distinct) variable restriction +