From c296abed04af39c7ba37b685dfe9c8239704d1c8 Mon Sep 17 00:00:00 2001 From: Zachary Bonagura Date: Mon, 23 Dec 2024 23:49:14 -0500 Subject: [PATCH] Documentation and clean up code Documentation and clean up code --- Cargo.lock | 62 +++++------ aris/Cargo.toml | 5 +- aris/src/equivs.rs | 39 +------ aris/src/expr.rs | 28 +++++ aris/src/parser.rs | 37 +++++++ aris/src/proofs.rs | 83 +++++++++++++- aris/src/proofs/proof_tests.rs | 31 +----- aris/src/proofs/xml_interop.rs | 2 +- aris/src/rules.rs | 52 ++++----- auto-grader/Cargo.toml | 3 + web-app/src/components/proof_widget/mod.rs | 43 +++++++- web-app/static/index.html | 103 +++++++++++------- .../proofImages_light/Strong Induction.png | Bin 11237 -> 10079 bytes .../proofImages_light/Weak Induction.png | Bin 9678 -> 9568 bytes 14 files changed, 317 insertions(+), 171 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fc5b6388..e05a9e33 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1,6 +1,6 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. -version = 3 +version = 4 [[package]] name = "addr2line" @@ -28,9 +28,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.94" +version = "1.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7" +checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04" [[package]] name = "anymap2" @@ -335,7 +335,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13b588ba4ac1a99f7f2964d24b3d896ddc6bf847ee3855dbd4366f058cfcd331" dependencies = [ "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -359,7 +359,7 @@ dependencies = [ "proc-macro2", "quote", "rustc_version", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -515,7 +515,7 @@ checksum = "162ee34ebcb7c64a8abebc059ce0fee27c2262618d7b60ed8faf72fef13c3650" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -922,9 +922,9 @@ checksum = "884e2677b40cc8c339eaefcb701c32ef1fd2493d71118dc0ca4b6a736c93bd67" [[package]] name = "libc" -version = "0.2.168" +version = "0.2.169" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5aaeb2981e0606ca11d79718f8bb01164f1d6ed75080182d3abf017e6d244b6d" +checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" [[package]] name = "linux-raw-sys" @@ -994,9 +994,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.8.0" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" +checksum = "4ffbe83022cedc1d264172192511ae958937694cd57ce297164951b8b3568394" dependencies = [ "adler2", ] @@ -1044,9 +1044,9 @@ dependencies = [ [[package]] name = "object" -version = "0.36.5" +version = "0.36.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" +checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87" dependencies = [ "memchr", ] @@ -1240,7 +1240,7 @@ checksum = "3c0f5fad0874fc7abcd4d750e76917eaebbecaa2c20bde22e1dbeeba8beb758c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -1439,9 +1439,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.7" +version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" +checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834" dependencies = [ "bitflags 2.6.0", ] @@ -1574,15 +1574,15 @@ dependencies = [ [[package]] name = "semver" -version = "1.0.23" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" +checksum = "3cb6eb87a131f756572d7fb904f6e7b68633f09cca868c5df1c4b8d1a694bbba" [[package]] name = "serde" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" +checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e" dependencies = [ "serde_derive", ] @@ -1600,20 +1600,20 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" +checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] name = "serde_json" -version = "1.0.133" +version = "1.0.134" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377" +checksum = "d00f4175c42ee48b15416f6193a959ba3a0d67fc699a0db9ad12df9f83991c7d" dependencies = [ "itoa 1.0.14", "memchr", @@ -1745,9 +1745,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.90" +version = "2.0.91" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" +checksum = "d53cbcb5a243bd33b7858b1d7f4aca2153490815872d86d955d6ea29f743c035" dependencies = [ "proc-macro2", "quote", @@ -1828,7 +1828,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -1880,7 +1880,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -2075,7 +2075,7 @@ dependencies = [ "log", "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", "wasm-bindgen-shared", ] @@ -2110,7 +2110,7 @@ checksum = "30d7a95b763d3c45903ed6c81f156801839e5ee968bb07e534c44df0fcd330c2" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -2312,5 +2312,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] diff --git a/aris/Cargo.toml b/aris/Cargo.toml index 779f4a14..8016a30c 100644 --- a/aris/Cargo.toml +++ b/aris/Cargo.toml @@ -1,8 +1,11 @@ [package] name = "aris" version = "0.1.0" -authors = ["Avi Weinstock "] +authors = ["Avi Weinstock ", "Zach Bonagura "] edition = "2021" +description = "Aris is a formal logic proof-building tool designed to help users learn and practice logic." +repository = "https://github.com/Bram-Hub/aris" +license = "GPL-3.0" [dependencies] base64 = "0.21.0" diff --git a/aris/src/equivs.rs b/aris/src/equivs.rs index 6ea73fcb..20e2b333 100644 --- a/aris/src/equivs.rs +++ b/aris/src/equivs.rs @@ -35,13 +35,6 @@ define_rewrite_rule! { ("(P | Q) & (P | R)", "P | (Q & R)"), ] } -define_rewrite_rule! { - COMPLEMENT, - &[ - ("phi & ~phi", "_|_"), - ("phi | ~phi", "^|^"), - ] -} define_rewrite_rule! { IDENTITY, &[ @@ -63,29 +56,6 @@ define_rewrite_rule! { ("~_|_", "^|^"), ] } -define_rewrite_rule! { - ABSORPTION, - &[ - ("phi & (phi | psi)", "phi"), - ("phi | (phi & psi)", "phi"), - ] -} -define_rewrite_rule! { - REDUCTION, - &[ - ("phi & (~phi | psi)", "phi & psi"), - ("~phi & (phi | psi)", "~phi & psi"), - ("phi | (~phi & psi)", "phi | psi"), - ("~phi | (phi & psi)", "~phi | psi"), - ] -} -define_rewrite_rule! { - ADJACENCY, - &[ - ("(phi | psi) & (phi | ~psi)", "phi"), - ("(phi & psi) | (phi & ~psi)", "phi"), - ] -} // Conditional Equivalences define_rewrite_rule! { @@ -175,12 +145,6 @@ define_rewrite_rule! { ("(phi & psi) | (~phi & ~psi)", "phi <-> psi"), ] } -define_rewrite_rule! { - BICONDITIONAL_CONTRAPOSITION, - &[ - ("phi <-> psi", "psi <-> phi"), - ] -} define_rewrite_rule! { BICONDITIONAL_COMMUTATION, &[ @@ -247,10 +211,11 @@ mod tests { } } + /// Test function to verify the logical equivalence of rewrite rules using brute-force truth tables. #[test] fn bruteforce_equivalence_truthtables() { use std::collections::HashMap; - let rules: Vec<&RewriteRule> = vec![&*DOUBLE_NEGATION, &*DISTRIBUTION, &*COMPLEMENT, &*IDENTITY, &*ANNIHILATION, &*INVERSE, &*ABSORPTION, &*REDUCTION, &*ADJACENCY, &*CONDITIONAL_ABSORPTION, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_EXPORTATION, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_CONTRAPOSITION, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_REDUCTION, &*BICONDITIONAL_COMPLEMENT, &*BICONDITIONAL_IDENTITY, &*BICONDITIONAL_EQUIVALENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_SUBSTITUTION]; + let rules: Vec<&RewriteRule> = vec![&*DOUBLE_NEGATION, &*DISTRIBUTION, &*IDENTITY, &*ANNIHILATION, &*INVERSE, &*CONDITIONAL_ABSORPTION, &*CONDITIONAL_ANNIHILATION, &*CONDITIONAL_IMPLICATION, &*CONDITIONAL_CONTRAPOSITION, &*CONDITIONAL_EXPORTATION, &*CONDITIONAL_COMPLEMENT, &*CONDITIONAL_IDENTITY, &*CONDITIONAL_DISTRIBUTION, &*CONDITIONAL_REDUCTION, &*KNIGHTS_AND_KNAVES, &*CONDITIONAL_IDEMPOTENCE, &*BICONDITIONAL_ASSOCIATION, &*BICONDITIONAL_COMMUTATION, &*BICONDITIONAL_REDUCTION, &*BICONDITIONAL_COMPLEMENT, &*BICONDITIONAL_IDENTITY, &*BICONDITIONAL_EQUIVALENCE, &*BICONDITIONAL_NEGATION, &*BICONDITIONAL_SUBSTITUTION]; for rule in rules { for (lhs, rhs) in rule.reductions.iter() { println!("Testing {lhs} -> {rhs}"); diff --git a/aris/src/expr.rs b/aris/src/expr.rs index 0e6a9775..eb0b398e 100644 --- a/aris/src/expr.rs +++ b/aris/src/expr.rs @@ -861,6 +861,9 @@ impl Expr { normalize_expr(self) } + /// Normalize biconditional contrapositions in the expression. + /// Converts expressions of the form '(A <-> B)' into their negated counterparts '(~A <-> ~B)'. + /// Ensures that this transformation does not occur repeatedly to avoid infinite loops. pub fn normalize_biconditional_contraposition(self) -> Expr { self.transform(&|expr| { match expr { @@ -924,6 +927,7 @@ impl Expr { } } + /// Helper function for collecting unique expressions under absorption laws fn collect_unique_exprs_absorption(expr: &Expr, op: Op, unique_exprs: &mut BTreeSet) { match expr { Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { @@ -947,6 +951,9 @@ impl Expr { } } + /// Normalize an expression using absorption laws: + /// Simplifies redundant subexpressions like 'A | (A & B)' => 'A'. + /// Handles associative operators to simplify expressions with nested terms. pub fn normalize_absorption(self) -> Expr { if let Expr::Assoc { op, exprs } = self { let mut unique_exprs = BTreeSet::new(); @@ -965,6 +972,8 @@ impl Expr { } } + /// Helper function for collecting expressions to reduce over logical reduction rules + /// Applies rules like 'A & ~A' -> '⊥' or 'A | ~A' -> '⊤'. fn collect_reduction_exprs(expr: &Expr, op: Op, reduced_exprs: &mut BTreeSet) { match expr { Expr::Assoc { op: expr_op, exprs } if *expr_op == op => { @@ -1004,6 +1013,9 @@ impl Expr { } } + /// Normalize an expression using logical reduction rules: + /// Simplifies contradictions ('A & ~A') to '⊥' and tautologies ('A | ~A') to '⊤'. + /// Reduces nested expressions based on their logical structure. pub fn normalize_reduction(self) -> Expr { match self { Expr::Assoc { op, exprs } => { @@ -1047,6 +1059,8 @@ impl Expr { } } + /// Check if an expression is a subset of another associative expression. + /// Used to validate containment relationships between subexpressions. fn is_subset_of_assoc(expr: &Expr, set: &BTreeSet, op: Op) -> bool { match expr { Expr::Assoc { op: expr_op, exprs } if *expr_op == op => exprs.iter().all(|sub_expr| set.contains(sub_expr)), @@ -1054,6 +1068,8 @@ impl Expr { } } + /// Normalize adjacency in expressions: + /// Simplifies and flattens expressions with adjacent associative operators. pub fn normalize_adjacency(self) -> Expr { match self { Expr::Assoc { op, exprs } => { @@ -1076,6 +1092,7 @@ impl Expr { } } + /// Extract expressions from associative structures while preserving their operator type. fn extract_associative(self, op: Op) -> Vec { match self { Expr::Assoc { op: expr_op, exprs } if expr_op == op => exprs, @@ -1083,6 +1100,8 @@ impl Expr { } } + /// General simplification for associative expressions: + /// Attempts to merge or simplify pairs of subexpressions under a given operator. fn simplify_general(mut exprs: Vec, op: Op) -> Option { for i in 0..exprs.len() { for j in (i + 1..exprs.len()).rev() { @@ -1102,6 +1121,8 @@ impl Expr { } } + /// Try to simplify a pair of expressions based on logical relationships. + /// Merges or simplifies expressions under logical operators (e.g., 'A | B'). fn try_simplify_pair(e1: &Expr, e2: &Expr, op: Op) -> Option { match op { Op::Or | Op::And => Self::simplify_logic(e1, e2), @@ -1109,6 +1130,7 @@ impl Expr { } } + /// Attempt to simplify two associative expressions with the same operator. fn simplify_logic(e1: &Expr, e2: &Expr) -> Option { match (e1, e2) { (Expr::Assoc { op: sub_op1, exprs: exprs1 }, Expr::Assoc { op: sub_op2, exprs: exprs2 }) if *sub_op1 == *sub_op2 => { @@ -1127,6 +1149,7 @@ impl Expr { None } + /// Create an associative expression from a list of subexpressions. fn assoc_or_single(mut exprs: Vec, op: Op) -> Expr { exprs.sort(); exprs.dedup(); @@ -1136,6 +1159,7 @@ impl Expr { } } + /// Determine if two lists of subexpressions are complementary. fn is_complementary(others1: &[&Expr], others2: &[&Expr]) -> bool { matches!( (others1, others2), @@ -1513,6 +1537,8 @@ impl Expr { }) } + /// Infer and manipulate quantifiers: + /// Applies rules like '(∃x (P & Q))' => '(∃x P) & (∃x Q)' and merges compatible quantifiers. pub fn quantifier_inference(self) -> Expr { let distribute_quantifiers = |expr: &Expr| -> Option { match expr { @@ -1547,6 +1573,8 @@ impl Expr { self.transform(&|expr| distribute_quantifiers(&expr).map_or((expr.clone(), false), |transformed| (transformed, true))) } + /// Distribute quantifiers across associative operators: + /// Pushes quantifiers inside conjunctions or disjunctions when applicable. pub fn quantifier_distribution(self) -> Expr { let push_quantifier_inside = |kind: QuantKind, qname: String, exprs: &mut Vec| { exprs.iter_mut().for_each(|iter| { diff --git a/aris/src/parser.rs b/aris/src/parser.rs index 4e32f92b..66ebffcc 100644 --- a/aris/src/parser.rs +++ b/aris/src/parser.rs @@ -1,4 +1,18 @@ //! Parse infix logical expressions into an AST +//! +//! This file defines a parser for converting infix logical expressions into an Abstract Syntax Tree (AST). +//! It utilizes the 'nom' parser combinator library to handle parsing logic. The resulting AST can represent +//! various logical constructs, such as predicates, quantifiers, tautologies, contradictions, and operators +//! (e.g., AND, OR, IMPLIES). +//! +//! ## Main Functions +//! - 'parse': Converts a logical expression string into an AST ('Expr') or returns 'None' if parsing fails. +//! - 'parse_unwrap': Like 'parse', but panics on failure. Primarily used for testing. +//! +//! ## Grammar and Parsing Notes +//! - The parser handles infix logical expressions with support for parentheses, quantifiers, and operators. +//! - Functions are modular and correspond to specific grammar productions in Extended Backus-Naur Form (EBNF). +//! - The parser includes support for Unicode symbols (e.g., '∀', '∃', '∧', '∨'). use nom::branch::alt; use nom::bytes::complete::tag; @@ -36,10 +50,12 @@ pub fn parse_unwrap(input: &str) -> Expr { parse(input).unwrap_or_else(|| panic!("failed parsing: {input}")) } +/// Custom error helper function for parser failure fn custom_error(a: A) -> nom::IResult { Err(nom::Err::Error(nom::error::Error { input: a, code: nom::error::ErrorKind::Fail })) } +/// Parses a variable, ensuring it is not a reserved keyword fn variable(input: &str) -> nom::IResult<&str, String> { verify(variable_, |v| keyword(v).is_err())(input) } @@ -48,50 +64,62 @@ fn variable(input: &str) -> nom::IResult<&str, String> { // `alt` corresponds to alternation/choice in an EBNF grammar // `tag` is used for literal string values, and supports unicode +/// Matches whitespace characters (spaces or tabs) fn space(input: &str) -> IResult<&str, ()> { value((), many0(one_of(" \t")))(input) } +/// Matches variable-like identifiers (alphanumeric or underscores) fn variable_(input: &str) -> IResult<&str, String> { map(recognize(many1(one_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_"))), |v: &str| v.to_owned())(input) } +/// Matches logical keywords ('forall' or 'exists') fn keyword(input: &str) -> IResult<&str, &str> { alt((tag("forall"), tag("exists")))(input) } +/// Parses a logical contradiction (e.g., '_⊥_') fn contradiction(input: &str) -> IResult<&str, Expr> { value(Expr::Contra, alt((tag("_|_"), tag("⊥"))))(input) } +/// Parses a logical tautology (e.g., '⊤') fn tautology(input: &str) -> IResult<&str, Expr> { value(Expr::Taut, alt((tag("^|^"), tag("⊤"))))(input) } +/// Parses a negation term (e.g., '¬A') fn notterm(input: &str) -> IResult<&str, Expr> { map(preceded(alt((tag("~"), tag("¬"))), paren_expr), |e| Expr::Not { operand: Box::new(e) })(input) } +/// Parses a predicate or variable term fn predicate(input: &str) -> IResult<&str, Expr> { alt((map(pair(delimited(space, variable, space), delimited(tag("("), separated_list0(tuple((space, tag(","), space)), expr), tag(")"))), |(name, args)| Expr::Apply { func: Box::new(Expr::Var { name }), args }), map(delimited(space, variable, space), |name| Expr::Var { name })))(input) } +/// Parses a universal quantifier ('∀') and associates it with an expression fn forall_quantifier(input: &str) -> IResult<&str, QuantKind> { value(QuantKind::Forall, alt((tag("forall "), tag("∀"))))(input) } +/// Parses an existential quantifier ('∃') and associates it with an expression fn exists_quantifier(input: &str) -> IResult<&str, QuantKind> { value(QuantKind::Exists, alt((tag("exists "), tag("∃"))))(input) } +/// Parses any quantifier ('∀' or '∃') fn quantifier(input: &str) -> IResult<&str, QuantKind> { alt((forall_quantifier, exists_quantifier))(input) } +/// Matches whitespace characters after quantifier fn space_after_quantifier(input: &str) -> IResult<&str, ()> { value((), many1(one_of(" \t")))(input) } +/// Matches whitespace characters depending on if there exists a quantifier or not fn conditional_space(input: &str) -> IResult<&str, ()> { let is_next_quantifier = peek(quantifier)(input); @@ -101,6 +129,7 @@ fn conditional_space(input: &str) -> IResult<&str, ()> { } } +/// Parses a logical binder (quantifier + variable + body) fn binder(input: &str) -> IResult<&str, Expr> { map( tuple(( @@ -120,34 +149,42 @@ fn binder(input: &str) -> IResult<&str, Expr> { )(input) } +/// Parses an implication term (e.g., 'A -> B' or 'A → B') fn impl_term(input: &str) -> IResult<&str, Expr> { map(separated_pair(paren_expr, tuple((space, alt((tag("->"), tag("→"))), space)), paren_expr), |(left, right)| Expr::Impl { left: Box::new(left), right: Box::new(right) })(input) } +/// Parses an AND operator (e.g., '&', '∧', or '/\') fn andrepr(input: &str) -> IResult<&str, Op> { value(Op::And, alt((tag("&"), tag("∧"), tag("/\\"))))(input) } +/// Parses an OR operator (e.g., '|', '∨', or '\/') fn orrepr(input: &str) -> IResult<&str, Op> { value(Op::Or, alt((tag("|"), tag("∨"), tag("\\/"))))(input) } +/// Parses a biconditional operator (e.g., '<->' or '↔') fn biconrepr(input: &str) -> IResult<&str, Op> { value(Op::Bicon, alt((tag("<->"), tag("↔"))))(input) } +/// Parses an equivalence operator (e.g., '===' or '≡')/// Parses an equivalence operator (e.g., '===' or '≡') fn equivrepr(input: &str) -> IResult<&str, Op> { value(Op::Equiv, alt((tag("==="), tag("≡"))))(input) } +/// Parses an addition operator ('+') fn plusrepr(input: &str) -> IResult<&str, Op> { value(Op::Add, tag("+"))(input) } +/// Parses a multiplication operator ('*') fn multrepr(input: &str) -> IResult<&str, Op> { value(Op::Mult, tag("*"))(input) } +/// Parses a sequence of associative terms and their operators fn assoc_term_aux(input: &str) -> IResult<&str, (Vec, Vec)> { alt(( map(tuple((paren_expr, delimited(space, alt((andrepr, orrepr, biconrepr, equivrepr, plusrepr, multrepr)), space), assoc_term_aux)), |(e, sym, (mut es, mut syms))| { diff --git a/aris/src/proofs.rs b/aris/src/proofs.rs index fbcecbf4..7522771b 100644 --- a/aris/src/proofs.rs +++ b/aris/src/proofs.rs @@ -165,7 +165,7 @@ pub mod pooledproof; /// - Trivial to construct from Claim objects /// ## Cons /// - Doesn't support most operations -/// - Doesn't handle binding structure, so can't be used for first order logic, only prepositional logic +/// - Doesn't handle binding structure, so can't be used for first order logic, only Propositional logic pub mod java_shallow_proof; /// A LinedProof is a wrapper around another proof type that adds lines and strings, for interfacing with the GUI @@ -202,57 +202,130 @@ pub trait Proof: Sized { type JustificationReference: Clone + Eq + Ord + Hash; type SubproofReference: Clone + Eq + Ord + Hash; type Subproof: Proof; + + /// Creates a new proof object. + /// This initializes an empty proof structure. fn new() -> Self; + + /// Retrieves the top-level proof of the current proof structure. + /// The top-level proof is the outermost subproof that encapsulates all lines and subproofs. fn top_level_proof(&self) -> &Self::Subproof; + + /// Looks up the expression associated with a premise reference. fn lookup_premise(&self, r: &Self::PremiseReference) -> Option; + + /// Looks up the justification associated with a justification reference. fn lookup_step(&self, r: &Self::JustificationReference) -> Option, Self::SubproofReference>>; + + /// Looks up a subproof using its reference. fn lookup_subproof(&self, r: &Self::SubproofReference) -> Option; + + /// Mutates the expression of a premise in place. + /// The provided closure is executed on the mutable reference to the expression. fn with_mut_premise A>(&mut self, r: &Self::PremiseReference, f: F) -> Option; + + /// Mutates the justification of a step in place. + /// The provided closure is executed on the mutable reference to the justification. fn with_mut_step, Self::SubproofReference>) -> A>(&mut self, r: &Self::JustificationReference, f: F) -> Option; + + /// Mutates a subproof in place. + /// The provided closure is executed on the mutable reference to the subproof. fn with_mut_subproof A>(&mut self, r: &Self::SubproofReference, f: F) -> Option; + + /// Adds a new premise to the proof. + /// Returns a reference to the newly added premise. fn add_premise(&mut self, e: Expr) -> Self::PremiseReference; + + /// Adds a new subproof to the proof. + /// Returns a reference to the newly added subproof. fn add_subproof(&mut self) -> Self::SubproofReference; + + /// Adds a new step (justification) to the proof. + /// Returns a reference to the newly added step. fn add_step(&mut self, just: Justification, Self::SubproofReference>) -> Self::JustificationReference; + + /// Prepends a step to the proof, adding it at the beginning. + /// If no steps exist, adds it as the first step. fn prepend_step(&mut self, just: Justification, Self::SubproofReference>) -> Self::JustificationReference { match self.lines().first() { Some(first_step) => self.add_step_relative(just, first_step, false), None => self.add_step(just), } } + + /// Adds a premise relative to another premise reference. + /// The `after` parameter determines if the new premise is added before or after the reference. fn add_premise_relative(&mut self, e: Expr, r: &Self::PremiseReference, after: bool) -> Self::PremiseReference; + + /// Adds a subproof relative to another justification reference. + /// The `after` parameter determines if the new subproof is added before or after the reference. fn add_subproof_relative(&mut self, r: &JsRef, after: bool) -> Self::SubproofReference; + + /// Adds a step relative to another justification reference. + /// The `after` parameter determines if the new step is added before or after the reference. fn add_step_relative(&mut self, just: Justification, Self::SubproofReference>, r: &JsRef, after: bool) -> Self::JustificationReference; + + /// Removes a line from the proof using its reference. fn remove_line(&mut self, r: &PjRef); + + /// Removes a subproof from the proof using its reference. fn remove_subproof(&mut self, r: &Self::SubproofReference); + + /// Retrieves all premise references within the proof. + /// Returns a vector of premise references. fn premises(&self) -> Vec; + + /// Retrieves all justification and subproof references within the proof. + /// Returns a vector of mixed references. fn lines(&self) -> Vec>; + + /// Retrieves the parent subproof of a given line reference, if it exists. fn parent_of_line(&self, r: &PjsRef) -> Option; + + /// Verifies a specific line in the proof to check its validity. fn verify_line(&self, r: &PjRef) -> Result<(), ProofCheckError, Self::SubproofReference>>; + /// Retrieves the expression for a given proof reference, or `None` if not found. fn lookup_expr(&self, r: &PjRef) -> Option { r.clone().fold(hlist![|pr| self.lookup_premise(&pr), |jr| self.lookup_step(&jr).map(|x| x.0)]) } + + /// Retrieves the expression for a proof reference, returning an error if not found. fn lookup_expr_or_die(&self, r: &PjRef) -> Result, Self::SubproofReference>> { self.lookup_expr(r).ok_or_else(|| ProofCheckError::LineDoesNotExist(r.clone())) } + + /// Retrieves a premise expression or returns an error if the reference is invalid. fn lookup_premise_or_die(&self, r: &Self::PremiseReference) -> Result, Self::SubproofReference>> { self.lookup_premise(r).ok_or_else(|| ProofCheckError::LineDoesNotExist(Coproduct::inject(r.clone()))) } + + /// Retrieves a justification or returns an error if the reference is invalid. fn lookup_justification_or_die(&self, r: &Self::JustificationReference) -> Result, ProofCheckError, Self::SubproofReference>> { self.lookup_step(r).ok_or_else(|| ProofCheckError::LineDoesNotExist(Coproduct::inject(r.clone()))) } + + /// Looks up a premise or justification, returning either type wrapped in a coproduct. fn lookup_pj(&self, r: &PjRef) -> Option)> { r.clone().fold(hlist![|pr| self.lookup_premise(&pr).map(Coproduct::inject), |jr| self.lookup_step(&jr).map(Coproduct::inject)]) } + + /// Retrieves a subproof or returns an error if the reference is invalid. fn lookup_subproof_or_die(&self, r: &Self::SubproofReference) -> Result, Self::SubproofReference>> { self.lookup_subproof(r).ok_or_else(|| ProofCheckError::SubproofDoesNotExist(r.clone())) } + + /// Returns all direct justification references in the proof. fn direct_lines(&self) -> Vec { self.lines().iter().filter_map(|x| Coproduct::uninject::(x.clone()).ok()).collect() } + + /// Returns all proof references, including premises and direct justification lines. fn exprs(&self) -> Vec> { self.premises().into_iter().map(Coproduct::inject).chain(self.direct_lines().into_iter().map(Coproduct::inject)).collect() } + + /// Retrieves all justifications within the proof, optionally including premises. fn contained_justifications(&self, include_premises: bool) -> HashSet> { let mut ret = self.lines().into_iter().filter_map(|x| x.fold(hlist![|r: Self::JustificationReference| Some(vec![r].into_iter().map(Coproduct::inject).collect()), |r: Self::SubproofReference| self.lookup_subproof(&r).map(|sub| sub.contained_justifications(include_premises)),])).fold(HashSet::new(), |mut x, y| { x.extend(y); @@ -263,6 +336,9 @@ pub trait Proof: Sized { } ret } + + /// Computes the transitive dependencies of a specific line in the proof. + /// Returns a set of all lines that the given line depends on. fn transitive_dependencies(&self, line: PjRef) -> HashSet> { use frunk_core::coproduct::Coproduct::{Inl, Inr}; // TODO: cycle detection @@ -290,6 +366,9 @@ pub trait Proof: Sized { } result } + + /// Determines the depth of a specific line in the proof hierarchy. + /// Returns the number of subproof levels enclosing the line. fn depth_of_line(&self, r: &PjsRef) -> usize { let mut result = 0; let mut current = r.clone(); @@ -300,6 +379,8 @@ pub trait Proof: Sized { result } + /// Computes all possible dependencies that a given line can reference. + /// Updates the provided sets of valid dependencies and subproof references. fn possible_deps_for_line(&self, r: &PjRef, deps: &mut HashSet>, sdeps: &mut HashSet) { // r1 can reference r2 if all of the following hold: // 1) r2 occurs before r1 diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index a40df43f..2136a985 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -67,7 +67,7 @@ macro_rules! enumerate_subproofless_tests { test_commutation_bicon, test_association_bool, test_association_bicon, test_demorgan, test_idempotence, test_doublenegation, test_distribution, test_complement, test_identity, test_annihilation, test_inverse, test_absorption, - test_reduction, test_adjacency, test_resolution, test_tautcon, test_empty_rule, + test_reduction, test_adjacency, test_resolution, test_truth_func_conseq, test_empty_rule, test_modus_tollens, test_hypothetical_syllogism, test_disjunctive_syllogism, test_constructive_dilemma, test_destructive_dilemma, test_halfdemorgan, test_strengthen_antecedent, test_weaken_consequent, test_con_intro_negation, @@ -826,22 +826,20 @@ pub fn test_complement() -> (P, Vec>, Vec>) { let r16 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r5)], vec![])); let r17 = prf.add_step(Justification(p("_|_"), RuleM::Complement, vec![i(r6.clone())], vec![])); let r18 = prf.add_step(Justification(p("^|^"), RuleM::Complement, vec![i(r6)], vec![])); - let r33 = prf.add_step(Justification(p("_|_ & P"), RuleM::Complement, vec![i(r32.clone())], vec![])); - let r34 = prf.add_step(Justification(p("_|_ & P & X & F"), RuleM::Complement, vec![i(r32)], vec![])); - let r20 = prf.add_step(Justification(p("^|^ & ^|^ & _|_ & _|_"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r21 = prf.add_step(Justification(p("^|^ & (B <-> B) & (C <-> ~C) & (~D <-> D)"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r22 = prf.add_step(Justification(p("(A -> A) & ^|^ & (C <-> ~C) & (~D <-> D)"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r23 = prf.add_step(Justification(p("(A -> A) & (B <-> B) & _|_ & (~D <-> D)"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r24 = prf.add_step(Justification(p("(A -> A) & (B <-> B) & (C <-> ~C) & _|_"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); let r25 = prf.add_step(Justification(p("_|_ & _|_ & ^|^ & ^|^"), RuleM::ConditionalComplement, vec![i(r19.clone())], vec![])); - let r26 = prf.add_step(Justification(p("^|^ & ^|^ & _|_ & _|_"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r27 = prf.add_step(Justification(p("^|^ & (B <-> B) & (C <-> ~C) & (~D <-> D)"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r28 = prf.add_step(Justification(p("(A -> A) & ^|^ & (C <-> ~C) & (~D <-> D)"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r29 = prf.add_step(Justification(p("(A -> A) & (B <-> B) & _|_ & (~D <-> D)"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r30 = prf.add_step(Justification(p("(A -> A) & (B <-> B) & (C <-> ~C) & _|_"), RuleM::BiconditionalComplement, vec![i(r19.clone())], vec![])); let r31 = prf.add_step(Justification(p("_|_ & _|_ & ^|^ & ^|^"), RuleM::BiconditionalComplement, vec![i(r19)], vec![])); + let r33 = prf.add_step(Justification(p("_|_ & P"), RuleM::Complement, vec![i(r32.clone())], vec![])); + let r34 = prf.add_step(Justification(p("_|_ & P & X & F"), RuleM::Complement, vec![i(r32)], vec![])); (prf, vec![i(r7), i(r9), i(r12), i(r14), i(r16), i(r17), i(r21), i(r28), i(r29), i(r30), i(r33)], vec![i(r8), i(r10), i(r11), i(r13), i(r15), i(r18), i(r20), i(r22), i(r23), i(r24), i(r25), i(r26), i(r27), i(r31), i(r34)]) } @@ -866,7 +864,6 @@ pub fn test_identity() -> (P, Vec>, Vec>) { let r10 = prf.add_step(Justification(p("_|_"), RuleM::Identity, vec![i(r3)], vec![])); let r11 = prf.add_step(Justification(p("A"), RuleM::Identity, vec![i(r4.clone())], vec![])); let r12 = prf.add_step(Justification(p("_|_"), RuleM::Identity, vec![i(r4)], vec![])); - let r14 = prf.add_step(Justification(p("~A & B"), RuleM::ConditionalIdentity, vec![i(r13.clone())], vec![])); let r15 = prf.add_step(Justification(p("A & B"), RuleM::ConditionalIdentity, vec![i(r13.clone())], vec![])); let r16 = prf.add_step(Justification(p("~A & ~B"), RuleM::ConditionalIdentity, vec![i(r13)], vec![])); @@ -895,7 +892,6 @@ pub fn test_annihilation() -> (P, Vec>, Vec>) { let r10 = prf.add_step(Justification(p("A"), RuleM::Annihilation, vec![i(r3)], vec![])); let r11 = prf.add_step(Justification(p("^|^"), RuleM::Annihilation, vec![i(r4.clone())], vec![])); let r12 = prf.add_step(Justification(p("A"), RuleM::Annihilation, vec![i(r4)], vec![])); - let r14 = prf.add_step(Justification(p("^|^ & ^|^"), RuleM::ConditionalAnnihilation, vec![i(r13)], vec![])); let r16 = prf.add_step(Justification(p("^|^"), RuleM::ConditionalAnnihilation, vec![i(r15)], vec![])); @@ -930,16 +926,12 @@ pub fn test_absorption() -> (P, Vec>, Vec>) { let r1 = prf.add_premise(p("A & (A | B)")); let r2 = prf.add_premise(p("A & (B | A)")); - let r3 = prf.add_premise(p("A | (A & B)")); let r4 = prf.add_premise(p("A | (B & A)")); - let r5 = prf.add_premise(p("(A & B) | A")); let r6 = prf.add_premise(p("(B & A) | A")); - let r7 = prf.add_premise(p("(A | B) & A")); let r8 = prf.add_premise(p("(B | A) & A")); - let r9 = prf.add_premise(p("((A | B) & A) & (((A | B) & A) | C)")); let r10 = prf.add_step(Justification(p("A"), RuleM::Absorption, vec![i(r1)], vec![])); @@ -969,38 +961,32 @@ pub fn test_reduction() -> (P, Vec>, Vec>) { let p8 = prf.add_premise(p("D | (~A & (~~A | B))")); let p9 = prf.add_premise(p("P & M & (~P | Q)")); let p10 = prf.add_premise(p("P | M | (~P & Q)")); - let p11 = prf.add_premise(p("~P & (P | Q)")); let p12 = prf.add_premise(p("P & M & (~(P & M) | Q)")); let p13 = prf.add_premise(p("(forall A (A & B)) | (~(forall A (A & B)) & C)")); - let p14 = prf.add_premise(p("¬A | (A & B) | ¬C | (C & D)")); let r1 = prf.add_step(Justification(p("A & B"), RuleM::Reduction, vec![i(p1.clone())], vec![])); let r2 = prf.add_step(Justification(p("~A & B"), RuleM::Reduction, vec![i(p2.clone())], vec![])); let r3 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p3.clone())], vec![])); let r4 = prf.add_step(Justification(p("~B | A"), RuleM::Reduction, vec![i(p4.clone())], vec![])); - let r6 = prf.add_step(Justification(p("A"), RuleM::Reduction, vec![i(p1)], vec![])); let r7 = prf.add_step(Justification(p("A | B"), RuleM::Reduction, vec![i(p2)], vec![])); let r8 = prf.add_step(Justification(p("B"), RuleM::Reduction, vec![i(p3)], vec![])); let r9 = prf.add_step(Justification(p("B & A"), RuleM::Reduction, vec![i(p4)], vec![])); - let r10 = prf.add_step(Justification(p("B & (C | ~A)"), RuleM::Reduction, vec![i(p6.clone())], vec![])); let r11 = prf.add_step(Justification(p("B & (C & ~A)"), RuleM::Reduction, vec![i(p6)], vec![])); let r12 = prf.add_step(Justification(p("A | (~A & B)"), RuleM::Reduction, vec![i(p7)], vec![])); let r13 = prf.add_step(Justification(p("D | (~A & B)"), RuleM::Reduction, vec![i(p8)], vec![])); - let r14 = prf.add_step(Justification(p("P & M & Q"), RuleM::Reduction, vec![i(p9.clone())], vec![])); let r15 = prf.add_step(Justification(p("(P & M) | Q"), RuleM::Reduction, vec![i(p9)], vec![])); let r16 = prf.add_step(Justification(p("P | M | Q"), RuleM::Reduction, vec![i(p10.clone())], vec![])); let r17 = prf.add_step(Justification(p("(P | M) & Q"), RuleM::Reduction, vec![i(p10)], vec![])); - let r18 = prf.add_step(Justification(p("~P & Q"), RuleM::Reduction, vec![i(p11.clone())], vec![])); let r19 = prf.add_step(Justification(p("P & M & Q"), RuleM::Reduction, vec![i(p12.clone())], vec![])); let r20 = prf.add_step(Justification(p("(forall A (A & B)) | C"), RuleM::Reduction, vec![i(p13)], vec![])); - let r21 = prf.add_step(Justification(p("¬A ∨ B ∨ ¬C ∨ D"), RuleM::Reduction, vec![i(p14.clone())], vec![])); + (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r19), i(r18), i(r10), i(r12), i(r13), i(r14), i(r16), i(r20), i(r21)], vec![i(r6), i(r7), i(r8), i(r9), i(r11), i(r15), i(r17)]) } @@ -1020,10 +1006,8 @@ pub fn test_adjacency() -> (P, Vec>, Vec>) { let r2 = prf.add_step(Justification(p("A"), RuleM::Adjacency, vec![i(p2.clone())], vec![])); let r3 = prf.add_step(Justification(p("(B | A) & (A | ~B)"), RuleM::Adjacency, vec![i(p1.clone())], vec![])); let r4 = prf.add_step(Justification(p("(~B & A) | (A & B)"), RuleM::Adjacency, vec![i(p2.clone())], vec![])); - let r5 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p1)], vec![])); let r6 = prf.add_step(Justification(p("B"), RuleM::Adjacency, vec![i(p2)], vec![])); - let r7 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p3)], vec![])); let r8 = prf.add_step(Justification(p("Q"), RuleM::Adjacency, vec![i(p4)], vec![])); let r9 = prf.add_step(Justification(p("A & M"), RuleM::Adjacency, vec![i(p5.clone())], vec![])); @@ -1047,7 +1031,6 @@ pub fn test_resolution() -> (P, Vec>, Vec>) { let r2 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p1.clone()), i(p3.clone())], vec![])); let r3 = prf.add_step(Justification(p("_|_"), RuleM::Resolution, vec![i(p3.clone()), i(p4)], vec![])); let r4 = prf.add_step(Justification(p("a1 & a2"), RuleM::Resolution, vec![i(p3.clone()), i(p6.clone())], vec![])); - let r5 = prf.add_step(Justification(p("a1 | a2 | c | b1 | b2"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); let r6 = prf.add_step(Justification(p("a1 | a2 | b1"), RuleM::Resolution, vec![i(p1.clone()), i(p2.clone())], vec![])); let r7 = prf.add_step(Justification(p("a1 | a2"), RuleM::Resolution, vec![i(p5.clone()), i(p3.clone())], vec![])); @@ -1058,7 +1041,7 @@ pub fn test_resolution() -> (P, Vec>, Vec>) { (prf, vec![i(r1), i(r2), i(r3), i(r4)], vec![i(r5), i(r6), i(r7), i(r8), i(r9), i(r10)]) } -pub fn test_tautcon() -> (P, Vec>, Vec>) { +pub fn test_truth_func_conseq() -> (P, Vec>, Vec>) { use self::coproduct_inject as i; use crate::parser::parse_unwrap as p; let mut prf = P::new(); @@ -1071,22 +1054,18 @@ pub fn test_tautcon() -> (P, Vec>, Vec>) { let r2 = prf.add_step(Justification(p("^|^"), RuleM::TruthFunctionalConsequence, vec![i(p1.clone())], vec![])); let r3 = prf.add_step(Justification(p("A"), RuleM::TruthFunctionalConsequence, vec![i(p1.clone())], vec![])); let r4 = prf.add_step(Justification(p("~~~((A & ~B) | ~C)"), RuleM::TruthFunctionalConsequence, vec![i(p1.clone())], vec![])); - let r5 = prf.add_step(Justification(p("_|_"), RuleM::TruthFunctionalConsequence, vec![i(p2.clone())], vec![])); let r6 = prf.add_step(Justification(p("^|^"), RuleM::TruthFunctionalConsequence, vec![i(p2.clone())], vec![])); let r7 = prf.add_step(Justification(p("A"), RuleM::TruthFunctionalConsequence, vec![i(p2.clone())], vec![])); let r8 = prf.add_step(Justification(p("~~~((A & ~B) | ~C)"), RuleM::TruthFunctionalConsequence, vec![i(p2)], vec![])); - let r9 = prf.add_step(Justification(p("A"), RuleM::TruthFunctionalConsequence, vec![i(p3.clone())], vec![])); let r10 = prf.add_step(Justification(p("B"), RuleM::TruthFunctionalConsequence, vec![i(p3.clone())], vec![])); let r11 = prf.add_step(Justification(p("A | B"), RuleM::TruthFunctionalConsequence, vec![i(p3.clone())], vec![])); let r12 = prf.add_step(Justification(p("A & B"), RuleM::TruthFunctionalConsequence, vec![i(p3)], vec![])); - let r13 = prf.add_step(Justification(p("A"), RuleM::TruthFunctionalConsequence, vec![i(p4.clone())], vec![])); let r14 = prf.add_step(Justification(p("B"), RuleM::TruthFunctionalConsequence, vec![i(p4.clone())], vec![])); let r15 = prf.add_step(Justification(p("A | B"), RuleM::TruthFunctionalConsequence, vec![i(p4.clone())], vec![])); let r16 = prf.add_step(Justification(p("A & B"), RuleM::TruthFunctionalConsequence, vec![i(p4.clone())], vec![])); - let r17 = prf.add_step(Justification(p("B"), RuleM::TruthFunctionalConsequence, vec![i(p1), i(p4)], vec![])); (prf, vec![i(r1), i(r2), i(r3), i(r4), i(r6), i(r9), i(r11), i(r13), i(r15), i(r17)], vec![i(r5), i(r7), i(r8), i(r10), i(r12), i(r14), i(r16)]) diff --git a/aris/src/proofs/xml_interop.rs b/aris/src/proofs/xml_interop.rs index 692a970d..f9790e57 100644 --- a/aris/src/proofs/xml_interop.rs +++ b/aris/src/proofs/xml_interop.rs @@ -31,7 +31,7 @@ pub fn proof_from_xml(r: R) -> Result<(P, ProofMetaData), Str let s: &str = $x; match crate::parser::parse(&s) { Some(e) => e, - None if s == "" => Expr::Var { name: "__xml_interop_blank_line".into() }, + None if s == "" => Expr::Var { name: "".to_string() }, None => return Err(format!("Failed to parse {:?}, element stack {:?}", s, element_stack)), } }}; diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 44c6734b..f5d60652 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -46,12 +46,12 @@ Each `check` implementation usually starts off with bringing the rules of the re Adding the tests and implementing the rule can be interleaved; it's convenient to debug the implementation by iterating on `cargo test -- test_your_rule_name`, possibly with `--nocapture` if you're println-debugging. ## Checklist for adding a new rule type -(e.g. for adding `PrepositionalInference` if it wasn't already there) +(e.g. for adding `PropositionalInference` if it wasn't already there) - Create the new enum, preferably right after all the existing ones - Add the new enum to the `Rule` type alias, inside the `SharedChecks` and `Coprod!` wrappers - Add a `RuleT` impl block for the new enum - if default metadata applies to all rules of the type, add those (e.g. `BooleanEquivalence`) - - if default metadata doesn't apply to all rules of the type, add an empty match block (e.g. `PrepositionalInference`) + - if default metadata doesn't apply to all rules of the type, add an empty match block (e.g. `PropositionalInference`) */ use crate::equivs; @@ -80,7 +80,7 @@ use strum_macros::*; #[allow(missing_docs)] #[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum PrepositionalInference { +pub enum PropositionalInference { AndIntro, AndElim, OrIntro, @@ -235,7 +235,7 @@ pub struct EmptyRule; #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub struct SharedChecks(T); -pub type Rule = SharedChecks; +pub type Rule = SharedChecks; /// Conveniences for constructing rules of the appropriate type, primarily for testing. /// The non-standard naming conventions here are because a module is being used to pretend to be an enum. @@ -283,20 +283,20 @@ pub mod RuleM { // If the parens are omitted, $value:tt only captures SharedChecks, without the (...) // I haven't yet found a way to use macro_rules! to convert between expr and pat. declare_rules! { - [AndIntro, "CONJUNCTION", (SharedChecks(Inl(PrepositionalInference::AndIntro)))], - [AndElim, "SIMPLIFICATION", (SharedChecks(Inl(PrepositionalInference::AndElim)))], - [OrIntro, "ADDITION", (SharedChecks(Inl(PrepositionalInference::OrIntro)))], - [OrElim, "DISJUNCTIVE_ELIMINATION", (SharedChecks(Inl(PrepositionalInference::OrElim)))], - [ImpIntro, "CONDITIONAL_PROOF", (SharedChecks(Inl(PrepositionalInference::ImpIntro)))], - [ImpElim, "MODUS_PONENS", (SharedChecks(Inl(PrepositionalInference::ImpElim)))], - [NotIntro, "PROOF_BY_CONTRADICTION", (SharedChecks(Inl(PrepositionalInference::NotIntro)))], - [NotElim, "DOUBLENEGATION", (SharedChecks(Inl(PrepositionalInference::NotElim)))], - [ContradictionIntro, "CONTRADICTION", (SharedChecks(Inl(PrepositionalInference::ContradictionIntro)))], - [ContradictionElim, "PRINCIPLE_OF_EXPLOSION", (SharedChecks(Inl(PrepositionalInference::ContradictionElim)))], - [BiconditionalIntro, "BICONDITIONAL_INTRO", (SharedChecks(Inl(PrepositionalInference::BiconditionalIntro)))], - [BiconditionalElim, "BICONDITIONAL_ELIM", (SharedChecks(Inl(PrepositionalInference::BiconditionalElim)))], - [EquivalenceIntro, "EQUIVALENCE_INTRO", (SharedChecks(Inl(PrepositionalInference::EquivalenceIntro)))], - [EquivalenceElim, "EQUIVALENCE_ELIM", (SharedChecks(Inl(PrepositionalInference::EquivalenceElim)))], + [AndIntro, "CONJUNCTION", (SharedChecks(Inl(PropositionalInference::AndIntro)))], + [AndElim, "SIMPLIFICATION", (SharedChecks(Inl(PropositionalInference::AndElim)))], + [OrIntro, "ADDITION", (SharedChecks(Inl(PropositionalInference::OrIntro)))], + [OrElim, "DISJUNCTIVE_ELIMINATION", (SharedChecks(Inl(PropositionalInference::OrElim)))], + [ImpIntro, "CONDITIONAL_PROOF", (SharedChecks(Inl(PropositionalInference::ImpIntro)))], + [ImpElim, "MODUS_PONENS", (SharedChecks(Inl(PropositionalInference::ImpElim)))], + [NotIntro, "PROOF_BY_CONTRADICTION", (SharedChecks(Inl(PropositionalInference::NotIntro)))], + [NotElim, "DOUBLENEGATION", (SharedChecks(Inl(PropositionalInference::NotElim)))], + [ContradictionIntro, "CONTRADICTION", (SharedChecks(Inl(PropositionalInference::ContradictionIntro)))], + [ContradictionElim, "PRINCIPLE_OF_EXPLOSION", (SharedChecks(Inl(PropositionalInference::ContradictionElim)))], + [BiconditionalIntro, "BICONDITIONAL_INTRO", (SharedChecks(Inl(PropositionalInference::BiconditionalIntro)))], + [BiconditionalElim, "BICONDITIONAL_ELIM", (SharedChecks(Inl(PropositionalInference::BiconditionalElim)))], + [EquivalenceIntro, "EQUIVALENCE_INTRO", (SharedChecks(Inl(PropositionalInference::EquivalenceIntro)))], + [EquivalenceElim, "EQUIVALENCE_ELIM", (SharedChecks(Inl(PropositionalInference::EquivalenceElim)))], [ForallIntro, "UNIVERSAL_GENERALIZATION", (SharedChecks(Inr(Inl(PredicateInference::ForallIntro))))], [ForallElim, "UNIVERSAL_INSTANTIATION", (SharedChecks(Inr(Inl(PredicateInference::ForallElim))))], @@ -522,9 +522,9 @@ pub fn do_expressions_contradict(prem1: &Expr, prem2: &Expr) -> Result ) } -impl RuleT for PrepositionalInference { +impl RuleT for PropositionalInference { fn get_name(&self) -> String { - use PrepositionalInference::*; + use PropositionalInference::*; match self { AndIntro => "∧ Introduction", AndElim => "∧ Elimination", @@ -544,7 +544,7 @@ impl RuleT for PrepositionalInference { .into() } fn get_classifications(&self) -> HashSet { - use PrepositionalInference::*; + use PropositionalInference::*; use RuleClassification::*; let mut ret = HashSet::new(); match self { @@ -558,7 +558,7 @@ impl RuleT for PrepositionalInference { ret } fn num_deps(&self) -> Option { - use PrepositionalInference::*; + use PropositionalInference::*; match self { AndElim | OrIntro | OrElim | NotElim | ContradictionElim => Some(1), ContradictionIntro | ImpElim | BiconditionalElim | EquivalenceElim => Some(2), @@ -567,7 +567,7 @@ impl RuleT for PrepositionalInference { } } fn num_subdeps(&self) -> Option { - use PrepositionalInference::*; + use PropositionalInference::*; match self { NotIntro | ImpIntro => Some(1), AndElim | OrIntro | NotElim | ContradictionElim | ContradictionIntro | ImpElim | AndIntro | BiconditionalElim | EquivalenceElim => Some(0), @@ -577,8 +577,8 @@ impl RuleT for PrepositionalInference { #[allow(clippy::redundant_closure)] fn check(self, p: &P, conclusion: Expr, deps: Vec>, sdeps: Vec) -> Result<(), ProofCheckError, P::SubproofReference>> { - use PrepositionalInference::*; use ProofCheckError::*; + use PropositionalInference::*; match self { AndIntro => { if deps.len() == 1 { @@ -1696,7 +1696,7 @@ where premise = premise.sort_commutative_ops(restriction); conclusion_mut = conclusion_mut.sort_commutative_ops(restriction); } - let mut p = normalize_fn(premise.clone()); + let mut p = normalize_fn(premise); let mut q = normalize_fn(conclusion_mut); if commutative { p = p.sort_commutative_ops(restriction); @@ -1705,7 +1705,7 @@ where if p == q { Ok(()) } else { - Err(ProofCheckError::Other(format!("{p} and {q} are not equal. {:?}", premise))) + Err(ProofCheckError::Other(format!("{p} and {q} are not equal."))) } } diff --git a/auto-grader/Cargo.toml b/auto-grader/Cargo.toml index 95ef6edd..cdf7ad3d 100644 --- a/auto-grader/Cargo.toml +++ b/auto-grader/Cargo.toml @@ -3,6 +3,9 @@ name = "aris-auto-grader" version = "0.1.0" authors = ["Avi Weinstock "] edition = "2021" +description = "Aris is a formal logic proof-building tool designed to help users learn and practice logic." +repository = "https://github.com/Bram-Hub/aris" +license = "GPL-3.0" [dependencies] aris = { path = "../aris" } diff --git a/web-app/src/components/proof_widget/mod.rs b/web-app/src/components/proof_widget/mod.rs index dfb719c8..ff31e4b2 100644 --- a/web-app/src/components/proof_widget/mod.rs +++ b/web-app/src/components/proof_widget/mod.rs @@ -1,3 +1,8 @@ +/*!This file implements a Yew-based frontend component for editing, displaying, and managing natural deduction + * proofs in a structured UI. It provides mechanisms for creating, editing, and validating proofs interactively, + * with support for keyboard shortcuts, line dependency management, and UI-specific data handling. The file includes + * utility functions, enums, and a main component (ProofWidget) that manages the state and rendering of the proof editor. */ + mod actions; use crate::box_chars; @@ -37,6 +42,8 @@ use wasm_bindgen::JsCast; use js_sys::Math::random; +/// Retrieves the document object of the current web page. +/// This is used for DOM manipulation and event listeners. fn document() -> web_sys::Document { web_sys::window().expect_throw("window is undefined").document().expect_throw("document is undefined") } @@ -124,6 +131,8 @@ pub struct ProofWidgetProps { } impl ProofWidget { + /// Renders a checkbox for managing line dependencies. + /// This checkbox is interactive if the dependency is valid, otherwise it is disabled. fn render_line_num_dep_checkbox(&self, ctx: &Context, line: Option, proofref: Coprod!(PjRef

,

::SubproofReference)) -> Html { let line = match line { Some(line) => line.to_string(), @@ -231,6 +240,7 @@ impl ProofWidget { } } + /// Renders a UI widget for a justification line, including its dependencies and rule selector. fn render_justification_widget(&self, ctx: &Context, jref:

::JustificationReference) -> Html { let just = self.prf.lookup_justification_or_die(&jref).expect("proofref should exist in self.prf"); @@ -278,6 +288,9 @@ impl ProofWidget { } } + + /// Renders feedback for a specific proof line, such as correctness or errors. + /// Feedback includes messages for parse errors, valid premises, and rule violations. fn render_line_feedback(&self, proofref: PjRef

, is_subproof: bool) -> Html { use aris::parser::parse; let raw_line = match self.pud.ref_to_input.get(&proofref).and_then(|x| if !x.is_empty() { Some(x) } else { None }) { @@ -309,6 +322,8 @@ impl ProofWidget { } } } + + /// Renders a single proof line with all associated UI elements, including indentation, feedback, and actions. fn render_proof_line(&self, ctx: &Context, line: usize, depth: usize, proofref: PjRef

, edge_decoration: &str) -> Html { use Coproduct::{Inl, Inr}; let line_num_dep_checkbox = self.render_line_num_dep_checkbox(ctx, Some(line), Coproduct::inject(proofref)); @@ -437,6 +452,8 @@ impl ProofWidget { } } + /// Renders the entire proof structure as a hierarchical table. + /// Subproofs are displayed indented, with dependency management and line actions integrated. fn render_proof(&self, ctx: &Context, prf: &

::Subproof, sref: Option<

::SubproofReference>, line: &mut usize, depth: &mut usize) -> Html { // output has a bool tag to prune subproof spacers with, because VNode's PartialEq doesn't do the right thing let mut output: Vec<(Html, bool)> = Vec::new(); @@ -576,7 +593,9 @@ impl ProofWidget { } } -/// Is the user allowed to remove the line at `line_ref`? +/// Determines if the user is allowed to remove a line at `line_ref`. +/// Premises at the top level can only be removed if there are multiple top-level premises. +/// Steps can always be removed. fn may_remove_line(prf: &P, line_ref: &PjRef

) -> bool { use Coproduct::Inl; @@ -609,16 +628,14 @@ fn render_open_error(error: &str) -> Html { } } -/// Create a new empty premise, the default premise when creating a new one in -/// the UI. The `ProofUiData` is supposed to be modified so this appears blank. +/// Create a new empty premise, the default premise when creating a new one in the UI. fn new_empty_premise() -> Expr { - Expr::var("__js_ui_blank_premise") + Expr::var("") } /// Create a new empty step, the default step when creating a new one in the UI. -/// The `ProofUiData` is supposed to be modified so this appears blank. fn new_empty_step() -> Justification,

::SubproofReference> { - Justification(Expr::var("__js_ui_blank_step"), RuleM::EmptyRule, vec![], vec![]) + Justification(Expr::var(""), RuleM::EmptyRule, vec![], vec![]) } /// Create a new empty proof, the default proof shown in the UI @@ -637,6 +654,9 @@ fn new_empty_proof() -> (P, ProofUiData

) { impl Component for ProofWidget { type Message = ProofWidgetMsg; type Properties = ProofWidgetProps; + + /// Creates a new `ProofWidget` component. + /// Initializes the proof, UI data, and error handling based on the input properties. fn create(ctx: &Context) -> Self { ctx.props().oncreate.emit(ctx.link().clone()); let (prf, pud, error) = match &ctx.props().data { @@ -665,6 +685,9 @@ impl Component for ProofWidget { Component::update(&mut tmp, ctx, ProofWidgetMsg::Nop); tmp } + + /// Updates the `ProofWidget` state based on messages, such as line edits or rule changes. + /// This handles line actions, updates proof data, and re-renders the UI as needed. fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { let mut ret = false; if ctx.props().verbose { @@ -843,9 +866,15 @@ impl Component for ProofWidget { } ret } + + /// Handles property changes for the `ProofWidget` component. + /// Always triggers a re-render when properties change. fn changed(&mut self, _: &Context, _: &Self::Properties) -> bool { true } + + /// Renders the `ProofWidget` component. + /// Displays either the proof editor or an error message if the proof could not be loaded. fn view(&self, ctx: &Context) -> Html { let widget = match &self.open_error { Some(err) => render_open_error(err), @@ -863,6 +892,8 @@ impl Component for ProofWidget { } } + + /// Executes post-render logic, such as initializing Bootstrap submenus and popovers. fn rendered(&mut self, _: &Context, _: bool) { js_sys::eval("$('[data-submenu]').submenupicker(); $('[data-toggle=popover]').popover()").unwrap_throw(); } diff --git a/web-app/static/index.html b/web-app/static/index.html index a9761657..31a2f09c 100644 --- a/web-app/static/index.html +++ b/web-app/static/index.html @@ -1,57 +1,76 @@ - + - - + Aris - - - - - - - + + + + + + + - + - + - + - + - - - + diff --git a/web-app/static/proofImages_light/Strong Induction.png b/web-app/static/proofImages_light/Strong Induction.png index e1febab4be0fb1dbf892752bb1d98b2e9bf40fe0..c21a355beeba1e31b861e4dc42962cf5887b57b5 100644 GIT binary patch literal 10079 zcmbuFWmFtrx8_3xcW5MdaCc}tNPq-)2<{Nv9Rf7&?$Stb*Pww$f=h6BcWE4^^PhRw zy6?!HS$95kch%WdtLw<#_3ZsSVT$rnXvpu8U%h&T_E}m&`PD19BG_>XB0TK7W+Txb z_5I2y4cBq`#l_hUM2J8#nJ}#vW;XzU7%HxdWlWNOp9-{dPR7Ch0AxZ zDgM&w7V~8kgbxf10jO|Zu z?VPn8wQrFWxl%!aU4iR8=9SbSOtEmBUNj02W`g*-1R_PxmLd>K43VAhXK(@sHOWGt z5|hw7hJAA}M2dpuZEX2(f*sJe@As1rx?BWjSIGa~PUyyYRp~$PxesJFB{$QT8Edng zCvf8NjpFA*lt!f3Li?>FehOx0%@NBxar1FeVy4_L6KAJ#|E zR!AzLk*ftj1{l_#TKu<(sF*eT9*J<}VLg*Y55oCh2j)L9(csHl*2IOn zWBM0UohR1y6~_?({1LF?LS+)d!-JIXMeL9idXGKAL4sr#$P*ZpnCEox^vXySpjal@ ztzi#+;K~f50|g-6QFoN|Ld^N~(%K5!s}Q~Y%*#A!i!%#dR-k7jWL@H^U_v*=2W3pw z3eIiz{n;YH(>+6XFx{BEl#H9k)T0TCQTXGB=%04_;A;Fifjov%)VYA&Pr4&_@sT)i z+)DfT(}-hb?aFivI*&hiaETG*-PS#Rj|}BzTKPD?7kndNODl6TChu{GP|v)I_=iy)APrGL=h z{3wTPyF(T)b`F9PH8-d^9a+HEV@+hWrPG3GW!0*O!Z9QrrhC4@DG{@$)nYPp1Kxv| zk*udfuI-6~sM2%np?qh8WrEJEGVz1q;rxyyhguzimkVc!mIWNl#)p&gvL+`S(Mboj z=|a=`cV8I+dCnwR!m__#KtKTbX>9dmNc}4-cJs!5HUeLg@mWjOdYWdp*g)42AvDiB0nu6%}a_ zFF8!241-k#lsUEEOw+69XD17>!}v3qPc0xT=gVDrPHlIQ<&57B5F3jd2m^=18i+F0 zXrG@c=M-0k%d@1k`kaUv|G4uD+et=o=qoR9iJ zY?Pm6(miU6xk$>I1V|HXtjbj$tE)QDWJ{Uw19-g2HAp<#IqDm(t;JY8&nv!>U9hh; z?Px`7Pl=xkI?bq?BpxG%w>5UC@@o$k(p`<JYA<3 zqwI$)1B*4 z3C7iD`(5K2^Bp=_WK@aVXATcsv(u=M^1fHMJe(<{8eCk4od!EC7F=Y{NGod6LDZK?nH_4UtWkDr_M;Cd03kaW(Kth@qc+ceF1khpYJKBQ=Htc zHpgq}e!uvTJbL#go#mNePbV}6>ol~3vPJZKR_D>4L5*S9WWt#Me%9mrbR7@5vfbS5 zTnq1D`FnVTD@oH6fc%ROUe!y$OR=6bQo-Wpz}M%Y?1YalNpe+1m^UduSu+W(1b6Xp z5Hh9|c)xqM<#bhAN?n0wt|p<$k&Meh6*FW_Q$5va?be`{lOdkoo#zLA zl@-$={(1K7s^9k@!GVSME>w$iRU8Qe#9E!P{aV}UbkLy?b=ebP|18Y1%HLblPS^z` zCeMIg@Q$H%=T&P0#%&#gqc+$rhuc2M(H+$(c|ddedxESVP7;2HS;Lki^rT4xv`Y8+ zKI@MEx28ufT`EPr$MossKrQb!y}df~K`qwz zcsH{^b=@xZ2zZrwkE|xgi#t0lO2%w0?)&5{nPlWoL8bW0*s1PgpUKOpuRgwqWY&Ew zyW@?EO%0Vej<4FU-ixGua#W|>-Tf4Z8c!JGYDI?25p<(B718F z2e!?S-*WNboG^=5_^-GtURJImzF@-oHLqCh<=$dVrRnETA&Q%^nhN>qFx*7htTe`DwU=og;~4F?o3q0 z^bMbfSX$!lMEG``hivvTMI-2C@ZH|d8S&!l*VV^qxBX>U&t)QgHetbs)oPjxW9(La z=)2!}PG=Eb*4&P6XI~Vx z#*M1*O5k#LJz+X2+qN&&10)lg1|I|k%7tj%dWhLn%UrT~t`rUrpojIdUnlT2Tgp7uJGP15P|JJonUA~fo&<_$mi?mb1j zUh)B*vtj_xYH{9sR*?_Xs4+azy~WpY_Rl8N0r2e!RU)dFSGe*^)4w`weVQ%Ye#0V2 z?fM|NRiAgx$`*wzcabfnvDMjWorqH= zN6u{_Uw?C<=0lDAtC```*ALc&{hL|$*Gh0P_6JwuCFQTMp@z8oZ$Zw4k#RwC4#|5b<;xeVXHIqDBy; zyb$C5=V2Q#lly?D7+&jg(5yEl9fj7vf1Q*6 zq7f2nH1R6X=e-%ct?l)PHp;KE5AXcZ_;gY^kx?oo)<3Q(GIdx6o`^h$J7jy>or%q$ z&}+$ZWrEPkj^1^S&Pa=pManhR+fV^2L2oz17tnQ|ge5(eZ$!)^qU$t_y+=$Q3FnZG z`)s7jcikUbsu_tdCSvhRPJ=eGzrxe<7DbY#u^1m-X}LiIHB5tBGXfmG3ec+K_*Wdp zY$Ta7-a_5RJkeLM^g2kC_|M4${9*@T^sJyzm6 zB0;*|xp&u{Y2wEDX=-Dn?bB2k&pty;DAWHWXsSk=&{7w{ru1qPyR$4z#A;4QiJa;QjN86?m1ZBeWkX!e#b#}hcCO3h*#FV6P#lC0i0eA*iQc~*Hxe4_wbyKV1JZFUy<<^sik zt+cc+?KYY#YAs95)y8dIah+3vyYK+@ue<-iV>_CencLBT)%6nE-X?l?ux$!SlDY{J z=^A5yZ@B)2>u$&VZJU*QJc_vu3XyzZN{xeZnBiEq5NEYu$fwzTMEivhijhU5rIxbL zS(22k;q?hq;N#O1XL1~+l;LoZzQI9TPR)Z60ZS#`v)O*30joZ_I(_{{&@p}f4Rk{{ z=)0{=SgJ^X1GyekSbq+YuT;GY{;ju;aKG2gQXhP>7;|4o=opVIL;Y(5^AXX6^Oo?c zQ1o_}szT~Dk3?|i@?5-B`|r$gTYIxClbIolNR-?6P63VUSIb0mJb5(rRmnA;SZT9q zq0=fEqL<{TN`SVSt&o_wMMMwZ!=OYRj}!A38B_jyup1y)5scu-LL$xAL7D-HW8az` zUAwArUJ~&|#^|ND6tnUjo4KsguDXkx;J|%0PtV+Z*Eh3m65J;os2JfFo<;PG-6$G# zC>C>?H%P&0e=QQrlePY*?!zQ#d=3xXS4K%xeH;f^@Vc3?vfLfrgO=ocG&76Fc za(d`biuWbK=qDtv_sP*#0*#xJw&suH79eKqMn#{ zI=<7GVa&kPr?_qZM(Qmu62|8BEYkKy0*X*`W(-Fg%hR5-Gsl(NZUaFXzK6{%i)N(? zt4xjiGpa1~G>As6_NFvyCPJDd>`(s*xtwN+hbw`0%=^1qPcSUYp`sy?ueN^I38&T- zWY-nEIRUKq75KoXfO=(l-_r1daeIRpHO&>d)^*iD-40<%j|0^oVbk&D)!zE?k>QXP zCRx$!R~!Ou^UyXZ`E6U#$KjLfIU*NQBA%7kPFDf?MYWSc&PiedIUV-u*}cgmO=mYV zBABL6aNcP3^-jjt5BJuNRs?H&0v9cCyvkt7?)Qc;X9_x)9vRXWBryo% zu{yQ=1Oh{a3?HZ-8$2*hj+O(&KS!Tk>>HeE>V%(p79z#jn%gBjL4NnNm=ji&WmR|2 z@iW)Sqd43pufsgy!tCHvkQd|A`CT^ER1OdWvXpHANp+aJ>NzW-@4OcK!h+-H0kGH; zLUg(9pM(CvN4yt$e-SKv<~#fGLGTXM3^gkXCEPU?iwlr|&-^__oIw5F&tHiBE`nA| zO+huG49nqEbcZbu-S`kS{%3xt9it}IQUAe!h=DP|8qL-1*Tc~-lZGq92yea>pN~QJ zH5){}&UM}8M(92-2KP1EZSJ!zwYlQ@RUr3(PLj?Kc~|yUeqlvV^MhychvLd{5unZk zYdVlO$?4|JWZ5RLH`P|p-j7&jVNl__)9v;?J%iN(EKT28I6V}6O8W!H zVT+<)g?!>{PbTrsMNFj#hM|fBO4D`es>+xpKmjMzMh)#qN`#$!g=@d_5$3vYXU++t zPiv&0Xj}Q2to6k@?D&|s#^27c3QUM2{v4W`D6Wg9o_P*rDz&Gt+$Y*E`Q-(Ba4R(L zcP>X&Fjn)bunua=urZyn7EEP;a?{{ao2=jJ~=5}Vs6 zOH**+lW;8!{q6`X(M#hSY;KYaF|4bxpXJtBXh*CIY526f6*$N4#}!Q?K)uWquWlTQ^9Jbgdqkmh^*BBvf2c40=S{B#K$Tb5r|KXA`#pTy#cy2 z|HANL^iR=%{4QJtNA;pH5kmpbqdX)sQ3&`fZqSB<37!R9YI(Y-Z5oyT2LF6hWasXA1s;^N*z z=ZjLVZP}0UQ!65E4Mn>Gy~#?0=kXF?wjO>?RcfRp9&x$AaL=S+W#}@=tCu9hc_P)I za(w05RNsEhIl^nQ2^3P6QTvh!e9HSh1r+m8fm`ZeR-~X$hx?j5gW~)rUHOhLWbBrM1qR_ks z*4RJpMWv!>pUmK|R3JAOvDNx;MEhG#5t;`oB9$HZT+zSQAnDsjP&hjqHfvt^;x^T# zu@7HmhAhbEjOkhD!RY{)_*2B$V@bbVdwoGLiIay(NEn7+#Rc!Fo5mGK#BMtbFTsD+ z^GJ3NuD!||EQ{%`wX87k@FEOWc*dz&pvClb2tn6*=XC0yeT}?gvQxgeSr#O&SVx|K zhI+PN_ux*{KpLq?#)Bp#Zj|31Kfxre~AL@eXqYg=JTGITQ7H}gv)eaW=n8-Z>TK(auc~w zuV19S3iXr=?vw(~Q~*<*X7U+O4+EeSCBYcMCWqVXRC>BWYUYPv@r2jVXUD>xX?^we zdK-ON(ytYYE-G8N*X*9k8g%HDzgoQRH``E=LISIy>XzPY^)c(l4(W(*tCkRE&YdE? zSRYdLFD8<1j~j`CNWT6 z*qg3prXgz*oBd1)78y(?H4d&6sp_&X%JcB5NzF=a-C$op^jnm=H;gjoU)fZ zt1;>2K6Tr0ppQX=PQQ;@EVu!(r_TEE+Xo4~bEwI5zmtv4O8jCXQ=O=w8F^Elg@dYg znwC1H!@30P17Yw1^$W5ZYk|omN%YXym1x8Er4r5Cv1Lu_7>6VKJk_i88keBlmeHN2 z8go2#fMz>f#QYt|Pe4zpXR#>ENC2U=hT%LPr-)lt&gb*e?B&DhdpcN*0}tj^=jWz`A3GdKs+;VV-i*Prw}pHLeIO_ zyA{4KIU%YKAIF_mI+uoneJi?UZ(ybWi^dk`O%|rDG|@|SjKjZWf4Tppy8Uk^6{dA6 zJrouio=uKiSgBk(8&*GWkG7}*C1mbm0&p0YKfqceaX7_?(JPFQXw%Lfzcs+~o-7rS z;=;<^I$?wqWPoG% zOyiYl5Oq0Iyn28xaU^V5BhC z%e>P6AFueg8U1(s^ItRlAe6WCVypcI0CJ}XBz!4}6oM@H+7@q2VxicU7K(A(G9SH7 zVX)nMSX5yvNyHTU{bEP6;Pge*+Jx#uP9LRQ22eJtfB?+Ify|mzg#woKW=Z_?f#$Q^ zUn)Zlf>nz=?5yPt6{T3jy*NuE-Fo)KEe!_CQuQ=g0E6czO(|d#OQ7Hn(yP=rKc&7-ErGH<^B&;5sJhqO~IjvlakheC>-)#sW%2G_{G& zeWuf10DVR$NEP@Mp*U!GmmJ~1W|8-zjP;Q4z^h44} z^)0D{#0QqcNPJiT`|@3$AJ{j}pW?^PKc%~J5U`L+kVtLRtCT&v7p5b*9>Wx5 zqguqBRnMMfZ*!KkuwWyP%4t7re<%PGmx`HD-EgGusoC3wvMnnSQ5P$;kk^@!8q3e; zh8wE>KB($JmC0aL#h>4}Q*sPM?%i?QM`VQv^T3ip?#yzXWkc2q)ALy@sAk*IT82TG zddJiHXur|euu>{6LFmUP(+j%c6(S6+D7Z5lGZvwfkyy270=Pgc(PZB@Qu2ah&6>&5 zI8YR`$_UBJ^_(@`AXUv*nIi}U6P?&B%-In_=bwPGpJ6KjW1GLczm-=~4#Bd40ac1O zOLCHE!92ZvH&C=;Te__t>vCtbSLexeg+|A>@Z%dYyQw6Ut}|y8c=fozrv2~KZgux0 zOef@h>b!x&9XP%%6^UP7m`NLzuw9CgRCYw3RCd%-R^cRluKNAWFjm1h)d|mn`-KJ@8z-(<7rWBH42RPm zk9ket*Bg%Y6Ys(mP2w$tlr73seltLK&jb&YxKn{3I@b$*@8_O*WTjr{NhAdm+^)hZ zD7;BhEe1IaP}~wuB48U>wup7iXn}CWG+}TtmO3+uZOGWakx&y$RQl4WF}<0MS$%o>Rq6+DoA%t?T(c z3DmBHtjZwki^Fi+owut7GXPnY*Q_=eIXdaMF<9u2bkGMmCIPm-Kzet98PjbcC|ff| z8C3#j6S!5Y{^aQ*9=F?5>pOk=uxXQ;a+-8j-v*hU!Qu~}U&PzQ30|@W{d%9vNLdVR zM%>jMdf<|iwXV`HMiq{Hw6p2I$r?!IjnEB7igx34Jm~HI1>EZ2b5B_qa zgbt=(4ev|O&%6nvtKVXHw>ZLoO<`V=G|%}Wj7=#O)eB{lR)A-@`hleJaexjxnC zZ~vGX9MVwH;E$ZtWqRiLc$&`0SoB2xZ zmtRtSJm2!-HA;+jNby&W9e&?QP$0)LE9P4#A7!$LdhNYUcPZ11{-(P1L`O%24~aBb zg({<--yHVEBbofv;^e zcqemPnXSV>3yO_Dos4P?ZE6^~<%`KqKwm*dZ}^()5#xJ1zKBnDw^i$Y6HBW2mPxzI z?xULhx_0%tI~RJzYP9qy&KsZf_lPtULoB0Rv6e;TRySy7*RH>gsUeu|Y?X879p|pl z>TT}OmKiP>AZ-mOn4AX3HuQMKwN zQm8G>E~e3-+*o%mP9XxrqC27Hf!2WXg#BtUec)ihStP+t`}|YuZl}+n6&!et&a3 zOS<0(xobBdtAWq&vxC$b4bygr!RkG0SbqCtOVfOop!?@B0zL+b$s;x-1=O8)?aV~9?LX`bh#7qH>v<%Fy4N}o_rZ&d@@=WBZZ%BQ717R(1Ol(5 z@0m*lG+-M z%no~1QX}(H1Q7JLqDijhA_F@;xt|9d*y!z;%<$E%qeTN9;Pzy@BoIA@lz@P=+P$k0 zF6VH)sGr(-$Ut$$u(F{Y!LX~1|Yz)s-K z#8>YICIBQ^K|JHN4?Rpkexc#tfhmI?s&V#zRBF`!RlvejD)#OV{7nya*j}PUw)>y3 zyr3X?05d6;?tjX|U_vfivj0mHOgCX}{!3laFAt+y5{Jm#d^nSp7Jt7%3DbQF!|?2s zJ>{7HJ%Qu%i3>GGHQV1;EGQKHp&rPh0DC}*6awLYNm3-ZLN)7u_D!BQ9SaC2`uCs(NRXn1quoc{P*(?mtO8G6cm%U>?d&zPs7ty zczx{sH~5Qj1FRIvX*(UIex1g%!1qOQ<@}CN)lv0YAZxoK?SV_|d$4AeR=+``)^Yiq z^=gHEUIejt*w;$x@i#Oyl!OoTpvU?1=i9avVQSCuUFTdMsWX1skD`n#hD*o>scV@2 z&^YAE;LQZ_+UF!$Avh940>KL(M+q`B6tqx?=)W4~--zJwmA-)DF}=jF zRAsklfXMk0rW({|(xOuO85)IrgfgCtuX@Vg5-4yFZ;&R@DKQ_};TY5qA*1JWv^dHM zv*WpCXQ>3dm~65eeJub&Fh!hOj0H{1_e%6;ajx2DrMjD!6;6AWPnn#k9Dkx*1De6ZEr9}xBR?KbDu(^ehA&Lx z(N9SIF6u@3+MeE}H1LiY7@2H(3B<@P^i(%7Jt?k+FkLRq=XoA0tcCT4CfWhWU71in zovsE^MXKfDvBlf=cI|&`Jri|oW(0Q%Bgy`uhS{dgk(mDKuwiWv2RQF?+`)D-A2IxN z_@Yp>sc?W6QZYK&TY}H%2bEo%<>co3)XL`TSD(6h@vuN742-cp%e6^*HucPvs^v+u z17o}`&l7YuVs&LqVp~K7;4_9`S-sw(G<0&q7R*cUt$67=Ty@d)g_{lcoLQ+-pq21G z6#$}hw4Lb25reN-Q{vO&hI8uKyK=s1Xd@uu$7D~VPuBZ^F532Fap5zor!U=RJ0G?x zL?R~dWdldis)M=jdN(CES1U-%3yr`{0-{#4PHr7t`%mnPjBs zY5BX%8WFDQXVUg8R$L2x%h$%;7%rP}El~~GP_IG~i-HsLm}b%*_W^l}bLLo5GS!^R zx?i^7vXf*EbHbCYW>$qU9gcIqr8Q!jc8+Va;sk(M;+Un3#aqzK^-1Ou?WoBNW(qa# zA0f_#-;25I(@2K4_sESJS}SWeIn$*1x#&`)p&IlxvF{8~O_HwQ@!}sD-vkjy3cpR)o?@!>_Q8{~6wYJ5 z@4xWfx2^0jz+KC2##>^0qZP3B42YX!Yc`uZ(o5&N_kEMw*amHH7=EWX+c|H^SoQqX z60+;!AGoxN|L1glOQjd^DRr8EkHqg=P!ohdW>A+Oop|)XG6IjZG58gR+ zzp0^ycUVM|KkqzCF?I^)C~m_v=e5^%FRA@)OH*yD9Xx$xc`)6lWcL22%D^-+ivpLU z&v?+wF*WlwZt*9G@Zpf|5UcxBU^cj$*@72YQBMH4xxE*qOrSOryKgk)CzJ7Kb-4d(?DWatv-*5 zPWSsCQQRD$hNkw|wFvS;VyTGSGryvyVmr@KY{xq}sw532RN>eDtRWU{st+oYl}#$! zjLJh+`XF~*TGJIjq1jCd(jvd9W;ywoZh>B#pH1j_tqeNT$;klWBV5*E-4%2#-~l3Z znfhw$3Q*1Kt`4xDZf@NHV!c}9Q3)eVy<9g=N&8)v=7xyI z%z|5{hHFG>6pY#|-&0j1R9R#{KC?d5BhD&48(DJQp)AqJrYOl03hnm38ZkGYxk&IP zu>CU(Z_O(zTTz`to%O|m0Xc&-z-&7^fbP467H{niA*Y(UixSe+d^*MJ0e-1Te_und zN6U{(CqFj|s93pSm3&pGF&mVG<4P_DtY8$nVf_%TUv%ty3KN_Mv{+c!-_km%^*M`E?KeZcNTkO&$3(ENTW<+lh%FW?9^7j182hc(Sv@bwlF10xZd4>MW8D;7{4qL|NR7LJEv7_m4U z3*^oit%C-d_qBG{g!D}J13h@OY9<^QM;!qQ@(q^;(L%W1TgRbHwVt|S8eX-S1xpP* zrA9gO@Yg8%>9eqB{z4eroEYoOhM~J$Vfjic{xIH6LkFE8opE((<76QGLp8E=QI3&` z|ApKr=4;o}4kgMdJH|12S06*o5$2qi+hB}*(Wa<-#zmLg$FgO;%WP@B(T+4f$~>u^ zCx5HW&G=4G;|3280+ZJ0P?D%pgaC7;jgD1Sn@9p}I*WO4wmTIlu>2wMy{ z+3v3l>>ltaVsMn;jsP=?@4oTst*+J>qXV@lRqJ)|nx*6-|oZTJyz9r*^?KpdWVPBQ`ta-ndIooM zY2|hJ!0j8AQq<^^CUad2;+D9d^{IbWZ)xNl_l+Aa4CNE9aEw?0!In5@1B$lwW$5j% zQ8^sHMo*9>rSV9I@6kpG)FRV4|87p`{W*)9JPWwEUb_g$8z>#DcL83;%b~R&X&Ptf z6jzOrFfacGw_P^&u#WeYdZpIW3Q^~Tyln`yn9mRe5|`wE)7eX`Kllr%-=O^Yk#2## zq|dijxGqe+9NU)SCpl8czTBk;kP%1loE znLa(?$J~Zs@K_EnuR~0glT7R%Q6y`TvE_kk+|-dZo93L-N%l?+G*lr}hn2-)BY4iL zE?1;*n^0xzFz6Xgc0w1MJlt|cT0xasFSu@C;Xvlb@RFv!m4`X1WZADzn`L~N;pXoZ zrC45N%o#p;VpVs+zs-nT$^?uGt6%t?m5i%(f9XBfY)LxjKgd8Er%+19093J`z%ZFq7p{tIDwZg*K;XPIW3BvVat z%>1rzu~#2g4*xY)S79vGvJcI&Q~r>y%lM8nj^XIBeuU_)^64|e@t0nXf;oBZ!Ul4h zkUP`8EW%^L?+Kb8REO+$>12#F9f=w~|^h?4lAYnKwU_XBp4)47gBP8V8D30B>C*I&x>ON6pl2PH8%) zK*s8$A1<+OGxfHo{9YF=r_IY}BD3Un-x1cmCl|T9`}^CFaUIyZM{y_M_l{pg4m@`4 z!ayOQYMsq==zg?W4DhNFFy%fspJi5T;BW3AvQk_zCODLp#JoEoc5+jES=oAF=u(_p zs}mq!Gphsat++mE4+8@iD>;xmu44Z1mY3I}{;E48KI?w%*r)$7R`?N4bT28iX5(FM z9G;9Ac~Dhz-FQV(OB)RgKy&Wk_BjHKb38$WgmyYXApfqflkDlZO;LcaojoSUi6}m=254>D|bv%EGyScgg zjs_c@%G^OisbV+ZG0aO{xbLLKDeQ4<%F+6H+_QgPsz#J2;gS-LgJbHu7NJ2qe=xQ# zidZiG*r*qA5}OS(H`e^tv5ubOm0?z`))p^$$OJLK>0#LtL;A||+L<0Wc44dsRa_+& zL_BF48p`#vn#u9-DL3t{tmxu^#i?kbw}g$vnfL33M<#c8w0>-9iK-3@z86&K?iqyQW@8Zf96Y*)=*~$4b_j=HrZ=C8_BI}zN(yH(ZNRcRz>G%Ro?)d>wMW6G zN;GTW2Rb8Cak;RrBw=>5C<)(m4?*G-k~Zn&G-COdXBoieo9`JWq8CTm-Y0mtpuBLq zfO6U)e4$!h5QTE5beB*@wq>uK!xm1k+y}}>A>3>Z#f#C<(r_quS*jth?X#KDK~pED z)l`(Zr+t<+!* zE?LxlXv0Bkt7o-8>oTXA62?5#xwYib8HtL(3B@{@ao=HNbhLMMIaa{GZ)35Mg{Xa@ zcPXD)^b&tact&Mk7ZGi)Nvri9S?L{Bs7k(;tbw$3|6srPZ@r#hl;=YF&~}|ZeTHs` zdCPUQbfxy8lsiF0JkO{f`zS{l$NH1Sn_)*b)H#SYF$t}N?MPpata5w$bhLZFt8ZJ_ z>T3mJ^o$qeY%bR4Gmo20c?rIppc%{5^AfZl5^eE3(_JgjkaL()O9fowzU)`^b;)nG zG-#E!H^|qevSBb~frdkGImfRtw@5>O*jq%U8A&+O8!|@@Ib_~bE`do6bCZAGw{kZ% zgp}3tm>Ko&AF<+&!G+v^4;H-Uq7$Bz&i1;r{UI0~ zW24-o`&O*7jxMdS7^vNL!L@VvIG$HORycvemj$y&>N`<^)n}KN?956kBk+jb^cgD7 zuXD59ElN}HRlth~T?33M&%eFez3n@eZeU`OV}SSuY>oFOin)lKhibV{zP#R}0$SdXH0%-Ld4O%4%?YMMYk9*_U%CrSelb{ z=P=AG{#ZbK_fdh;4%!Zn4#yN`k*UwV@dF8_x@)G}#cKzE?9HdSs+Mw%tzRiBFTZ(u zzP>iDl_zKVUZZD4V>MyP53RR*Y=%`k0Lw#v;LZ!XtcHj@_Pe$;ehKFNY_Q}-_2A8@ z!8T_4h@d<=%5z{6Mq7|V$*;}7jh~Xt1TbFQdNXhK~?uXoc{s60rm%UN7i*lWP zQM74ngq6h!cXVYp(dFk8TSR)aTudcv5%k>>Tn6HN_YLsY|Fhj%!$t@LJD7KCqbS^y z?2b!H5E*`QBXr?f!m5{AWbn4zf2h&ihx_~wtYy`5cs=I$<;H>rcZ&1}SAPU>T?UnR z-iwa_En7QW^(v)4TKCuByb6q+HySuMJCtjUykvUOGI|GlTG4v9feLJl%wrtA{8Bm? zRRc#4chjNA>jls;E6(rEjYqsHeY^l1^>7w2iw!!Ak`40XVmg7~bI{y~E+~Y*p9?L8 zcP>3Xb_H+aSJiThU%S;vm5a@$s*)9``J!)5ejl^&5A#_pzYDQ8@|U8R_<<4M<+R|c z1uEmj5US<7?X#L?C+;#z;f^J7`FI+&ka4vPjMF*ZlvZ?p1z&XSJ>Zz`L#WBTPGs$D zS6Yi0;w{~1AA1Sig0MGpljx*>(u59B%?hq-6~~I*5z6{HzSdh+!trLtg` zg!d7}5+yq}8VN9pa5uCwaJ^|l95>r#WDH$ zdKVwfc6GprqX+AxB0d4}W|80~Pd6C#r6#HH-U=r!pfdqH*Rxb9Kz5FdDl+kEhaABK8fd&LUvHz5sI{6a{>p@?-_APWfC&6=a-ZCK8k7+%wY3=BW8DAQQG-)6eY6^ zkb9{6J&{io|1g4|AVQl%9v?*}>d1vZMiQ_R7p^}yXo zk*tPp9}g>f@S9fwhiQMr%g6#xOW}_3EDHv*H$Y;v+Qe#Z44(^7*>@Cb)K{;G&fKYv z#ZvM+wAoX!NG*GluSs-g|NX>IJ8Eb^^-%mV-gf5eS(@voP)5;$$=Rr2)o6}~U$Z3l zDL0>%#n(*^(Z#mHch}9VN-!6Q0BEa2o?z8@pM?C$5=W*Hj8=ObxZg`(v)h}^{=6U_ z%q@^cpIs)nps-;_iQZ}EJIVXnCdD!B*H|dQ{EYTEc+UnfTUqKP=KIZ~*D9xagVzG?k5rL*|-vb<<0GrN`8YH2CqJZFq@mwm$9_oMiRe(bAmv z-tMDQ8ofBhyrX5Z4!k@!aPl)NuI2kDGj-o8)jQ+Uk|Xs!b8zb`&c~#fg$K#LjA{dh zj7-Fy{04~xme{#Mv(mLSj9KmAK|OvZ3eWvV&E3A=1g%kztwuSH#k*zBV>1Sf^nXh= zd01M=)2At@1}zG58ygJ5)r+yQnVl+nX?gds(i$=_+Aw;}X`HNZrPqKCZ*dgPUU-CZ z|BRQN)fd?*q;>4^J(i#V)#}qQ&@BfpD=Wth@6;G^OKNj-v_pRykG9!H;N}!%AE_c7 z8{`0ebOY3Cj#F6wmZ=N&1YN4nR<#h8=- zlmn4v8d=rY4ASscrDQot#V)Q0J<@3aqt?fsbbo5MQaoSl)5>Mo+pWaFe(?tswsag` zeHPrQap4r&U;mo!Ok26e2Tb1^NSOh_FE~mQZnNkw=IaqTWI=XSzR4`P*S8N@H_`y9 zQZRn~oaJEUcUv!*v?~vY)#`qTc8MwulvDz=Fy83>`Z#c6l@Ky^0KzWB0PsgeZq|%VDhsq(`d(7yEJ<5n#o^nr&BoKj3a? zzT*&Zqn6MjhdO4*G$Y3sQ2aE&zXJxR~7kfXX1e9d?nqie6{uaw(}j7twSy zCgpp$9h<|lWPByd<(k6{eS3vMSU5zGcio2iuu|>0CXIK^wO8#OG6#O0`;6Y~@5M** z%V(^=@M*r*-2V>WKGDgxiLc|??Ng$t%|&4tTi20}?lF+zvEP?j& zct7OhA`?bp2H{f3J3BX4;cPeB&r+Gn@UK)3%-PF00e<8W+mCbrTr^-QtUyOBk~Vk_eL`10w^|3 z&jpc9$UyUzo;n8!6Cnlye>WaI3=}qh#Gb77Y!H3vP`4|272hymUt&rJc*V;Pa!`KK z2}Z)yqczr-3Aw=j;6WCo>C%qh_LyC6UV47Ts%{G5zkID&*IVGR4@VwnoGC*vOdaX7 zAmkkZ2@)NItb+^x%gIIb<~ja%ku-$VTVrFP<-NvBhY)td#F6O~t2SJT5Mpo4B_b*^ znGC{ZQov$!Nsh+ZdLzVo{V4*}Ovs8Q}`E{i+{NeXZU47@@@VMW9j4@{PsdX5t2W z6!8yU2|;if*IZq4K)l- zNM5Gjb8d~e4#i>DtJEOO-vE#UczIuG4Et$5(D0Dzz7ayyBxjD>Hnui}A!b6>)=Pn| z;V@8^<}Y*f`NHOE;7xa(LKqcKx9K?i0q5@3+LT=+GD_Ur8}8SFZeC$}-l|Fr#CQ}k z-pN7x98T<3>tv2 z!67(dX@sWk=F{^0k!A`rrVtOPY5xbE`YDn8?>~|)-4AH~`YXXh{9hR4e?yf1{}q{~ zZ6-C5Qc@*$>) zIT^-nCexWo?%EieG(!L@?l0B-cBWzDFZ{f1ShuQJ62k#7q~nk={vXi%?}6U$ly&ph zQ)>Jfi+QPzoID&7Qx!Oen13&^b8z*a3>T+5)`9AJuG9Gc>(wS^SSl*mSFei@T@?t5 zU9q?%Mv?xxXOJWCrXCKrdh7@(9`!yCkL+i*^k&Z)N2z`Yz54$ai%v1JC%>@u6inGK ziOiHBNd9jqH(!_f%c4(Goh@uzRc*Rnj*MwLeMX|I-%D$7;4L4iBl}C;KNV7Cab7eB zC^NrOQC!dMXH^Lm+dmU2eLk4O&M;?}Qx2zOLFG(F;%?1?AeffJNQ0A*GbZ+%y*W(r zVpWMqmWF4;ri;QlMhefKh7GqR>tXa%C<+}%nu40TG4o5e?-!e-M)s1wtH$?e0#Q}O zNKYctXl{x$HAMv%XgRj}+kaXGZYvfFNd5@{mVR4||7915EwTQF`ac#Y_z%ca$8kg& zctI>EV-k^0VJXeq8Iri5QBW-mnNMgkAKwku-@bw2_8sC$vcT!Tjn(?4x+G7=T*3mMlC+bq+Qo z-$mafK$o@hwduR$rpYghwY-vEM$XFTbWErZTdvg;!>3nopCKUpr%!mrA`SM_P$ka;(Blq%h1 zyzcTt--EnG4>us~$|AGJr3J#U4_NSrp%aI6WgmU?2a@B(+rtAWgtxEE^Pgl91{H-v zi{GvHG$N$p?VS3u`@}G4J;QC7*J;Q=R<*wax-iLKOmP^I5(hu<-PYlzs@Y#$mLjlP ziZzi$r6OG$JMj}-F&R3d9h^?%(G+fNQM()j9x?@Ck}$JW%o$4_i0ilFMFqMOwscw} zrL0e^&`0uL{b_z^e39{8Zr8_L&Ow?XyJqpGhB4dvPJDj)=_{nGBYDh`)1?xH_^_Gz zRS--b*-Yw7t}r>ZjGg?beS%IBDXU&=EVpKHB{TZULsm!hXJd6n+k5qyqT+(^1+MjD zivRneH{TqudggC}FYqw-QBw8e@C9)ajLgtub=YA(DMPz7E+DZkf_4T(ik&x#>{V~y zU1gPNt*1s#61t|>(87DyQEuy<(07eHG94sQUM~Bl_G=bvTKZl^Jwt}?RROFpebc80 zMzUyYb)+e4KC5T{nf;}cWb^|FSK3yFym1zm6w7WF_9vs-IO?vV_<1kL67#^OT5?Ot z8U~gZpi@x*ml>Qqbl|l|VpRNMEa!i45Z#}lJ*TZ|H*SAXI>3||4wnJ)i>nf|2nl{n zSrjXhI?4OUjIb0-{Pu~8K>+p(gJ8%Y$ZsRTm*llz{)7IBo!L0Z<7FQKt^RZTz%hIIlO8v)!32^2 zZC;Vy3t6K~i`V8oV~xrEnb5|O`^V+FMN;qL2hS@(mN%pmLYZR3iJ6 zsoVAwgEF!zQ+pbI%N6E`Rdv}==-t?lb02#_Y6g6@KKk&uS%8qS!P$(+l%Big+?OU zzm^CtD_1TgA&8`x9$dAk?8F_%;Tf#oRt2WN4Hd^UTMY!gDkbOSiT_EfvIUNMF8A67 zL}^GtA^-uh+g?k1jL7!rG<;l_6;YjRvFdvs2>ciJg^rBg$xR-iy1a67ai1$`QlDiE ziPW-Ype5tygIyG{{?M63krT7vf)SC|AG&M1QcBG@Am@!NN+l4&ao!u#uh zfzFRv8R4PHp(&`0!F@lHAB^x_gwX<^5|#H&XN`w^DN;g%i!S*1-AD}k)gX;(qWW12 zzTf>>)1Gim?F|N3ec~~4li(Vw0Zv8iwJtU@9%YQU9l=Rv1O|Pm6)|1?eQ(XtA9+6LCA_)pEf2Ut{x>4KcDwaD0>_C`6W;AAH`_y-x;SBG>K&ePWz8pHTL7E zj~fl%-|nahK$h@(gDxlZOD(N*vF^Ox!a%;@DtQ;~<2C$Tv>PdWHqw!vvnk}L!2i=5 zQ<%gAi_|@1nVv7h`Xwe>YcaA9^iPkZ5Pu+!X%4H>+*~Juq%k!d7gRr>QQ^=&+Pz}BvpysB`V>$& zY=j27H8jwFA2%MHSZpbE9EdRvP%soWvU(S4)_4wBATL<={I2OFrP+$~&E)>tH&81! zJX6~2WR9L6%_#6gcRE6j271|0vFSoSv4jvCx*HCd3hUj7b*W(-B#Xb=60(FM#gc6MfVbJ`pRS0kPd>TD*x4+dLA4qE@Fb+`i^Sow4Y04 z58J4TP*-CcGvE>W?2A6P#O=6XOj<2G8;RJ^RgZh^hQfrSGyBVt`G!W1%FDTP&X@Z# zfa7Z$mZhR@Uf#EV0`5bfn8-fqra%W>xxhkSo)kIC`5)DsWXlMl7ama~Z(`c2VzYr^ z>tSoaW$8vMg7~W41+^>lV2JRq^<6FfoyLiRaIS^lef&=0HswDT-)HopJ(T6pA2^a>9b8ZB6 zxTJx{MjI!Jb>pc_P@0H#BMTgP{H>%k60O8Ad>puJAt`9N0jlM5&A`g3>gOzqv_KoC zJ(KR=j-!MI>PIQmAqnXCq3Rr4VpoGxt%{fP_ksL5)VO#-Pn%M{^^~}MT5vzyzI7#i zhG?qDz4x~v^ut8jKV6Vg|JURmQU>(59(s3-F+z%gx3rE{NSdnl(>y{>Ch1@6uo4tA zGvU~{|5BZmxKdFSI+3u3f8I(@2%8y@MxdZ(;~@S|g~{&KXUaGZf}#@1Zz*u;aHV|6V~7Y`j6yFFkm%iQ1b& QT63XfKP!EzmM{+bAG|?dVgLXD diff --git a/web-app/static/proofImages_light/Weak Induction.png b/web-app/static/proofImages_light/Weak Induction.png index 6bd99b09b0e3e79a07dcbd51aa5aab49a55d74b2..ee0b0ff2c613d4c3da72376ef4380511c243808e 100644 GIT binary patch literal 9568 zcmb7~Wn5fcw&roF(865`w_w3tf&{l~dqzK-7(LmQ+Ma1r!vDy3(sal{{z7SGhR7P{i}a#KpQKU}hGTeC`5VWu z29}^QB11h}Dp!K!D0anHCxi7rF7sZ$|K*Ut1bz3e{dC^m>NYb6s&Mn^^m4S%MNI6Q zjLx9O6>jtR8WLgUBOaavHTFVxGX$hHtI>)l!w@f%1fsJg426JR7lIfdiiS|o=)`!~ zdu3pHI`%i8ERakYT@FZRWA)p;M(k}$BPYG4dnEi%+FiRD>`G&+3zvWs7LK+QJ)imS z;%Saqk-IatOb{JS5pYRwCgTY}C{uHi@qLBAdEb1yOO+X*3>KbhhqLHUi!U=c(#!oJ z`yK68u-!CJnrO3OJk;68sB8SETY9uU2_LB5lbB6eVl6OjNPl5bzpH;(#(@!%l+Mm7 zOay#Aq)|GfVMFBQcf5~5ln?r#nnTHg00g7S4KjeUAaVG$O0v~p7LSl{j3kf@R%()_ zjIQlIKT0@{R2e)hLS>NU_?XBKTUrL-JF5Y}|34RkJe(H%>L&{d5d2XdtO!Wv!;qGV z`l|U?=vclCH&-`-rxg~dyuF3NAR$wU?P1i-sjs2GnsfPOAl>biH&voFB`2qtR_ zOVkYr2|pQc>To3X`!UwP!8g_wHam6qNp7D^7+qp*dCq_f{I%?5C&)@;WQ@kXyBk!L zITsvHbCcVj`q*yMz1owQ$1&hq>83$cheK1{k|^OGIMuK3Fbc!Qw0;i#TJ*F)07bkE zXyrM)G{<{+6Y5}XV zA5lMw-(2zt>_0WIFTC}yImCJn2FWmNqynTpgP5pIRuhR%K0!GXWOKR*rq&GiVY~Df z3u}YhosAA9<(c)%iHm_&cm6)jBBC%qrlxJPcZWCC&vrT-4`mD?nH8jN%FrQAM z!M9sCf~-b(#=08!&qY=F_f`=iWA~edd0QH7IW+CSAR1kn2G`e72|-v@hO!Gw#DT2g z)(J#uTupB&iz5sV373!zWYPJOSn()`WJz+EU(sQ4qj-8HpI?MFPGF6iz!)1If`B~C z5(=mDy;j=HTduX_4ywu-B)*LD+%I45mbW>G4RMlt$dHJLvQtpLMSjm8(;m>jj87a# zelWxu5dRvGjD(COonve@S0%Uqo2$klgsZ=$xl@Z2BS5L*3Rb38TqOG#aZRf&DfJ+` zl2D0(yG0|@HzynBC&FbqrWg4j5}ul-D}^spMvRQrg<)1{=GZ5blN&licV9oav0TM( zSLVE-Vx=|pLC2)0bP#LsXt5yPi9{sc6nCJrdojio8T<;vSag}!8X0gU#kmj%h& ztQ@P(XqfaJxEokxmAt3n00iLblB5?nPrL?TEkz}%M{ZQ|tbwP7DA=tVegZ{^oN~lt z6)MDAJgT0{I(Q&SZhku*hx{uM`HjA43DiQ-4$#UZtQ&%ESD$+a4{hq+3o`8u8ZTCAiHXo+sl&YDPmkp* zak0gFdYnVTFe!c^Y+!G~%f{r-pCXS2c!U~uEU!wmtqzqCuUCv==O~j-7q7mvo(8J{ ze0Sc2n3#HAWeX!y{q&}FPzW8@-Mknc=&Kf7|GMKcn!7zXp9BGwmf*{p@-nM)WEqm6 zhslBrqPK#YznX%+pHR0<;CA}AtXRn?rs~S|KbL>GeBg$0Q=APIHDOR++@LV0p{`Hp zhUmZim0Kny!%!3hp`EB;m*`0PfV_G`6rdUK0nN0lXRUQIqahMRC;WyPUQWN_|J$Pa z4?;9;55Qm+QdLqTI>nQT+Q8#gy04{x*J|MrS}?0Ys{#NVp)kk-F6X-<59JMNV@oC1 zD{$75Qv~p^$S?taF<7M}y&)f+Euk=EHqqSZ7o6s?-)jrqa()-DV0k=@S5jOr zi;ys@Z1U%jH5f~t(gy2sQ2YgPc~jt_06uTHwqS}}cpPM@$y1b?wb_DzN28BE z!JIV6qHEYH>71Ykoes?PsS9G(|8!t;u#PaFiRVMtkjio?2y1YYDijD3y4seT#j{&} zbmIOktU5qLW}!VNfW<@9KDqemY)7|qrhwB(1h;>*o;gXwqA0zl-A!ZdS5#1aR@bQw zDsdS%Bi){0Si#`oCUaW&@&Z=R?t*-?;DB6)hS)%z>k%w$yKTj2I6O9R(tAXoG_qt*3${82BzXd9TEBn zETNcYIi@XI>Nwa&e|bn>9j0YPR&B9@3uD3Bq&F^G}iJObKLB zoSxce^J%E0i|@E)s@eO{V^gN|x9UNS=v-Z+y7Cs5s5)N0a@s1UH;B|Pu6s$+FZ<*X zkq@6R&!e}f17PP)39W<&ei8N^-*>bdSt^i>=jKtObL>4e6^VBov0k|G z>G`TRg{@Y*^Ui&yxO0zLD3Z+?b)IB; z#uh*<-Usy>>%}-4rkqQNRx&UZF4Yd&=$|X?uQzqe93fe{V$Ty5 zt!8Dm=4f{HSN2PM*<2SZ>dH@=R!3GJrmPt|mi^iP?9ptzNFJAyL5;EDO|Ls=b<2R` zzU8>V)vwN#DFd;47{~a~LUfkrQS`!viovDgETdH_QzMp5PZVoQ0!6gE1Mdy0Ur+Ej z<>*w-dwe8gPbHx5OTMo|KHLZc5_|8-6FViVNn=c@W5oz7qKv=vphQTTkr9>{w z!=s}1aN3MxHGE)DM5vJsaIa-5f2T!NS$tohj*Y`Q@YIW{%9BA8%|G&l?n$E_XQv-+ zTE1tTTN$}Q{rE+Q6vCyp9Tgw0BBIt0+ik3I9m0*8Cky3(Zyz*d4C&6275z9TCWZcH zM}2BS2@&x|rA5a*_6xv!xT+s${KH>I zQz?6`6_I%+hdV$6`Fw1c6Lz}>t@+-t{k)Tu{)s)pZ0Io7Xazv>FT2>*yEJ~vd_js&Wii}SQj*1dx(CzD0=4`%R?{-&c9i=1&<6GbB(-tUq=HMIw3y%Re|vxfCY;Ey zGc@)>mxot$q>*zrrFGC@$$i3<WRqju9oJ z1@Z(;Hufv`V47;8yIlQl#{+qoz)<(8yI9%uXtMK* zwDgX_$A{qeJqA_v?9rp7#Mp~wik+v56|^`=rd?t`E>Hw_RNmwIY=&&Xx7rZxj zvNicl@y3IMjLXMYy=PRN*z&reCn`qb!!N4QT#2>XdFHScSUv1P{AKUJYRKy~+KMbQ zQzaO0&H8*-iT0ULCT`a<9|MzEZ%-sqCcgPkXYd30(Lk@7v-uxylH{_SVv!$%KEA#^ zdp(Izvpc4v_&B-kesdcZ31QAho{yJzw1SP0%<(0O!aA~#L79-(m-Fkzl3YXr!(*Do z?T#CcCI%xUC7pZr4(5p3?b=xnLPT;;V%)?vyw>@gFsxpIc=(oJn>dq6vfl0Y_C0iu zTBJ_U_LaJUo}OD$Vzdm4d;Ew%y>Pi)050Qkg1^P|wdbkJ()=JG(UE#kS34}=XtDAN ztKsIuGB@x3PHZnLTjMrVd`32fjl&-kr1|U^xV+^qf<&D^G6SAGxjqm;M7O& zka!{(6|Duet@&X(zw!9Zk7J(hp6~a7JLePMyGe&^J3HxW7X@qSuJLkY(G9*9CJy4m zJFWM_mb=*`Fim&aKwHrhu)meA$ehG6<;soN5P#bV9nlztxzQB7tfw~UzX)eLyTgdw zK9|&Q*!Q34uw)4sS?GQ)kNWE!7^js56&Y_lNn3KeN^V42Cc5n3=R{c>aoag4q05&%5Psvr6MK6gRH|h_*`iyc%4!+Rd@OdKmUdq}-b*{={?<*}QvF7j; zI22B)J4Y-R+}zB^Q0#`97m|A790-@+RO@`2W+cb{IC=LQYOjhXQgeT5>DBif{oh#@ z2n}@R*7WⓈyJ@%rqB}MxX3ZBNlos+V%z(ZnGm12g!eQYF2e0XS@wxx!BYB^Jk{% zJ`A_WS^Yzs0!!#4G5u%kf zTolU;_Z_5~56SdKlvWxmF(FRpA`5|Ib%8+N_c-Dkb?4{-%UTH?ynX$=Y1IpR<-L{q zPi?9Ekh;Qg-G?Kg<<{y@Xdx!0M{xXqyqu3enC*GVEk#+9U?YtS=@xOETk-|a69lsK z1bR#+^FBGt)_N8~lLWUK&xozq^{$%sHnP=r(X$!|CC8~|X@w)RhpR=h-wBpe%IeD( zjX&p#Tbh9;bzWQ0N5Tr=5vqGXilcR8SGAnP6GjGPV&cG|X;3(EIz6>y4ob18ySdMY znC^uXc@YS`{}JuNx@RK!?W1U+GV|LK=bS!+oIo$NAW5nmBWC+I?FLOZkN6Jl6*637 ztK8pSm`+WkD@$)@l9p78ezBh}uuTiT;~Rg+K3Qw8FhjV+_t*1D^t^a7@Q=G9#bW*u zQR8nZBo=XSa?%ZE+$2x|Mu)y`3T8K%a2XNl&Nq@_QI6wa6i~qqmHPGApt-T(^Y5qJJoK)n2h@lD~g(7T<~`R zuiadc5A>}3lkS5*L`0d=X)IR>@~X0zzYlt#i)YEkr;sq5?XcjfB=0Xt*`= zcj9btvxRbO8Ekq2?cq|Zg4K!XKuuj&%E{bw^m<)Vh3RzXFRQE1NbTiTqL-h4_A<#P zd8cK~t8~p$)`Tk)CNk@mhf^3BjaIV@r~46Smm2l|YHlA<{o_F4z41$WAY4hm-C|~W zt5Q~2xsM|Ic}*nGE>WENmDL{>y)1 zf5hsFd90d$b$W-m|7b%W8l=P$tkO@(^ z$t2bLfgFj zj&2SWo5NcWtT5D7Us~vs2#2xL&Fq3^bX-^hW&aMY{%hm<*+f=DNQsSA_|4xN|B_I8 z5xM_g8qkN6_2YcZV|3BLCqckqYfArz8_I9n7aG*v-)K|pHavb?Aj7+ID;W~~5`=nW zjeLSoUm*!^!ZZ_nToXaZ#CJ=(UxXbcz;Lh~=MpM?F2IF*Kj8IYLUNO+&HhRXR?5Gx zIB!h*H}0L0*fZT?`4e%YHWA@|QR*SU3TT)baK40JdN<2hT(sq?L|*HDfll zE}^E{1oZlEKlcn5FzHv0^}xaT--*463)>4h``}lQM1?RnugGwO*1RN0YimI3d&_9@ z+5K0k5KvFj9Ro%5YgTSvt^BIWv1!_wLz_GeL=43J$$U;!T5xYZAd|uB(|^(Lzc>fJ zOw^bEf(zVeibU|RBp?~Q6^k&DO%ezN$(W!n8ho3FPXm(lu>X4s{;!GpPr~qTfcgI{ zluQ?}dlII%^~Yw?i}PuiWT`1~fwvp+`gpl!vrNfBXJc`AwWj>^!^WBfg7H=YNXr0C z7xYI2bAA>%oxT`U2z03S*NX z6p!x}XrL~l9!50F&+$S$=_^{@??cNOQDVDfC0D@EH@1*~U`2Wuy;D8^6ECSE@ zFJ|>~oDGg{N~7_3^Q>ZT0pQ*UaHJ#lpGfC>Z3&Q`9@S~JS)B;{ zPg&!pRBs*A2D4eQ{E0N$b4HArdx`?kB%%>TDe-r-Y|nUzslArQm+0PGRhGVOE*1i^5Xz9;q_GV*qaGjMkDR=0 z4)=z4M$fC?T+)bE;Zv3}c{mDlwe2zs@Z_spPq~g$r5SxZClJ!f$KO^~Cf(VQPR_#2 zR6<>}jR0NL0)2}<4kbA|#EH?h4ZH8*Q>UbKH9#}uJC>MFN}Q1dg1d@J9@-ZZg?k8w20&`QA6qjEDG6jj z3*o@$eLctoE`(J4oP^UsW3w-C0tS+0{2S_n7lXe&H^D#dYz;Rpk_?c=pohCsHGB(z ztI7ZO0O$Xi&M;ut^0v=%yC(%Oa{|YjH4}pj*ywubC8m{2^#tdSsRaa~T&MYsagWne zKf4gCUeceva$wiobv|?4`5^E3;Ibb*XV96e_ZRtkhoRQ<=m5uOgxvKdnCatTJnqLp zhLnt{e_~|9C8rLrIu^&)y}u)2;>lc<=`*st{3sbO!^wrKbbb>&R@5PiHiLwJFLa<+A4~7F2ml3m7W-ltGE^RNlSzch#RJL4nKdpmga#@K(XOAel3>|i~ zxael`yl`{t z1L|zUjIe~11kw-bd7oa2Yl)~0URLBE-6%Rc9Z;6f%c@-pyq);CqGev2<1`Vso zH!YUG2$8D5S`B9xqyfKVr)d85O+{E3HCB?uKs%0liMl@y*n(y%XDE-x%cs4FisHqM zWcib9OTs181yQVFT%!WRJ<@p2oa5}*2mLSU!;BUaqpW~fXjgu#i0^}O8*MfrD*sEmgt+orN&TPa@{ z^~0J=PAa$j^sI%p)Vh|jQx^ucO@P~rETmQMpU0ME>lauwnBCC>vV~CX`>qXWdRBlm z{j(&zacP&2vt?yq5ZW zHeq1I4tl6A7sqNXC?Hu+iijYbG!+Y*lAKVdXmLBiWC65HLOf;9-7xKfl2aYh&Msgn zUx(k%OGdHqYZm3FGwq*^Sn@DN2tWx-+8p_Hyw~*E)ZVI%z24)&+$KpVR6h6?vE*Az zROMSPLMNUv(eN`zO^tc#IM-7{!ZjrOIU-C!SU00M4%Ai+=JH7AQEt%8Z2WH_M6R)% zdg=u!s~z!f+Ad>jGVemXY3#(>OWA-Us*Ee_?iS!pUw17C88e6~P6Rda6DtbPH`${~ z)ClRCfWcTaa-ZTh>2oHgr)}bUI}4SL6BozdECOPYN0RH8^3D}6KZg|Rg>Lvcuw}0q z;1=TIZVeA}vY06EY+PKJ?DO3V@tQ%H;Pv!2#;IhIF%OdS%~7IrHBGwdAzd6ujNxax#ql)zFZ5ne!X|Ot)^B>h$kHN7n$kB zZJ7OB5X`?q&LdhB*-de4z6+{b1AVwngn$Yp(f-71=Z|Gf*^ICDB+Sy#J510IF2(g_ z5Hsp18U$NTef=g>z8@lIj>&yrP81+V5__FXV`=&`m?EsUpVK9!+(mRZZ9HKdt|VRP z(~ZoXtMr6jL9uwdYZ$`8qkY?4)n}gNIG#urTf7LE%tG@;Ack!@-Ua9EiXof0<9w-2 zt~CqO7@n3mis=3p@z*Uf>#`Wz6p z==x&_ry7UWL{1lWWtgIlpkSB%oRe5XUMPP^o7s3q{_znvtbTC76!Fv9op8=dwA=XB z)jP&A&!dP2c?$~gb~yKPZCL$)Vq%v|tv%p}U__7Q!l8(InygYUa|S*>>L({myx+%= zZjofUm1I*opM3rk=d1+VjoTQ{H`lr}!&&B&v?MNi^e+2Vunv|&yx$v%Yg)(LwyLzt z9KFdh(_R@A0+?f|#ULSDo~J1hkc-Hz&R zI(hS$EWC3;7j&9{--!2rgdiww(Vy~AH(iPr^l^Uwczb4RgTqvfEp>}=JfjGhA|WS$ zpU1(82f__|)W4k4`3J9E1Rn_A)K4uv2|z#>G?QbjaNnuKBr9V`rl-aX_gCk@u{!8{NOv%?AYe`$bdzydAMN${FB!@G+UMLcr;$A$sySpX0l_JHpxD_q#(BhQh4lNX?P+V^I ze)qobJ^P${?&sV;GRds0$z-1O%slJ&{jDffWmz07ax5eyBpi7;DRm?yWC_IQ&j579 zwj(2$3-N~RrY;LXsvf8OiP%B4l2AhQs7rWy2Sr2dV>-*daYI7F?fK({+>&H>h=fFM zCNCwS>1}klf@whX{So72V)V$>+l7U?I2dIUCQI!@11)>Ann997SsM{N^0|u5WprfOZ4(^W7}D-)%$N2(oYuMJvxu)>`Zo`Uh`-5Ydh~_ z2&KHm!_teNO#1z#KPAYsr4D^HRj8WDdBX}0Z?|Sz1%N-wfaL&5d{`2Y$VxQ;0mS?; z3CK3e9vr9?rJDG((fvITVk9L4E|u6^6Ua~bF{3lF5g!OgG>R|7(nruUhl$oF&-2qC zy(Fe8Jy_Z11)s!~eN_bbNRYwu$cJ{WY0u?St6z@_x%U-thOVm(0%sxxwC&JH9Yf>* z;0b~uWQCkC$eqJ56DptFJQte86lQB&aY~L^?TdE2a*CB*d8~n>dPq;-=PBy=izao% z{}$0_F8e8`EDw_@gnh}Y<*|`X(+XxoqG)YXMj&F z(6m}trmk|D#|H3`Tf7_z6Z|9A;@!p#Rx+Fx@q128sF?pb4snn~;4?d-&~V_JLg4f8 zVR9HPSZemqu9n(h-P$2MJ|arNag$9SCQa?q&26~0(~a3w&i-&(wXxzjzM_*h&T5hl zH6;=8u;lVA+3wm$e*3CQ)rB(A*4SH0jN}Dw*K=2ArWRz|_D|@T@G-=BxcU?lBjR*u zVlU6aXfpi+xC75s&mAqo`i*rq?sE>geKp=nOmh1OzMPxox_L0CIi{FZk$92Wt+giGo;7nKa*?I$^f+!DB+ z*`fH8%4kZPfd^fc$8DBoPW{g)>u6BBnkfhD=gv9PYD?2Br{s}QXo)F+)u8Y<(nJ1KFG z20?~nj<2zLmbV05TYLkQ(a>lOsz7l7*>-QGy>OI4GTfG(zuZc>tBNvlG zE1xUJh5bM$Ai%K|9mmf$vO|B^xaGXP4boUna` zYvY~3%G7s+3#J}(y(8tjUtXdOkB>)mYl#nF4Km7Ym>5p!RWcmYF%CK3B@B&>W%OVQ zIA0BW=ppV)#dIjZ7DzHhOpKoSnTd_1P-ZK~`#1ts)1EArlWrCMYJ?w*R#$gPt6BPl zq+}DXcz3w&;G%Uw7E{j}2e)pFX|JWA2@-deF8K1N2>1mQ4z_NHitQ3ZL0KD^S;&Rn za|Y2JoiOeiDJk$fupAZJ_UP1wDb>lEhI~n3AF$;lxpa%cpxTG*{Md%9v*x=NZ{p?F z*M+f{NL$)w=$a8gw!5(kjqa zomekWYBlJ%+?gw!25TDkPbI%m73>Nn9yHv=b`e6s(8us|!3+lqd3Q=Cx&=qH(X}k2 z_OG!SooXGtAaxP~nLI{+7YsDECE7YUik~?7CXJgD7Lf;2n=Y#v+{)04^38EX+~dRj zXH=oJ;%D(S1#fRq;B-sZfcMzA^^A%ig`Zb0Otl&BhQIh_BJdMe1+d}7C`zB4kAu@6#8P&c z>wM9%A>2ZIA`RMslEzqG zVr=QEgk3Uh1D{&<`toK++bJwPf!Jm{w>!QtsNscP_&6)qb9ix2K+=CZ%r*ecEu{jgjtapc6b~6jezJF72jOr831Mn9J>R?N(wd=wgJLiWQ+sd}Bdb(P<0RWmTwQ)A+5wd4%@RJC1jgH z!9v4hl=Tx_TvDhC2mZ3J1JT)!ap`jxykI&|T%@uD(LU{lA5{|}%2j>uizo}i5vEiv zUj`hBSv16Vh#;`0s{QMN?XeSC#37MFW@HvEoxMef`VF3-_UIb+Owh%YHu_U(n<)6ls6B+sZs)o8r`Cdn?N=?FjVVliB%v9t1&%Q$2OUnmEOb_M zH~MMk`Pw~;O$;JSzx%d95lIH7GIlOo`+=q3MKQZ9hU!PsM7>bMc$>RsC_FYYfZ=qt4eb%+9%QRKGkrqzQD4~wZvHb?(8|2cJiw-2986~ zt>xdbH(PaU^2>e~CUA>4l%^j2ytOcH<#wa)o{x#F95I0B9pf)nO@z zr#GxqEoUD`s7!zq;;=CyR_jkgmiX_E?{gC&LULcis8miii0BTkN=sBH#x$Jq8JnAl zvAPU-?{1Szl6OpDzuGwO$WK1zty6`A#fsz|WE#qPKZJOqlsJPzaku5;7~XbB>{_8o ze0yooQk1%gU78#Sl$lWjWJ$Y0$JgLG!$g6n6?D430nf8o5;MMtXI>O?7096Fe`|Mx z}aM0+j7-N@>rrlE6v(lHeOZ!hlw zl(!Fr#C*LNc7bVn(XTsOjI9rtQmwzFg>OZ{A8WS1r(`gw>8|w2)E?I9wK%$;ElX;k zdcF37e(AYYe+pI^{HTztZ`oklPfjI+D`6-K67EF-zHlJ_K&GPcgzIs~ooTNtEU89M zq1o>x5#O53Nhw^FC~K%w(u>;ttl`v{_F%uwS~!q5qqJ!7#k&1k@Npu!VB>R2;ptpy zW)1u?MznlcdSn}npdqpVZe4GJ5t2KahF5o74dZ>yQCAOB_no;Kn$RWcuL?@@xK%AkHh_j->XW9;fP|d9hU7ln8=XE^c z`0D7EM4`dbBlx7Va#58U6m?u8lpBLzdzAzOjA1|M;C-)|(I=~pxzFk8y_XzyeXpT9 z%5qC#QPjk$g6=~fU&B{Qg2E!Q!?Le5#3hV6i9&6&jGD8}9a>WxJS5e}(MYd{cM$fHS-D-4ZmMO_@#6LXA1bZE`RCb-Ku+9RQ$15SgXgDc<0fAdx32q z*m{Mt6Dh7$c}53Z8TYa-XrE&_0G+us{+@8?$R@vXKcsat?P+3!7{AjH`?reS)w*p7 z<&wpce=In=w*Vw(R<@Ati$z{aV%!xW|N>g zZcQ|UHg^fbLz}x6b|Wua07PM=9irMU%n>GApaJuzT=~Uwq*)rSkP^+X-~ZT`nhYzw z%fLf#uk2c)r1Xt!eUKd@Z`{8%I2Z-EV!-r}se#PYraj(2nIWd#8kD!c_GSw0 zR6#a&5|r^`#zH!*>JxN-^Aw}T(%G`C(rOBDT%DcZn6d=~kw!o9iZ@-|T@dVT9?JU7 zGxeds{ne`x2Jhk|EFW3C4R0TT+t2e+nAx(>uY83m6bba=ZenP4x7s~H-h#?D_EQd{ zv@IVQ6{*4`BaVaJ9B?@cQ&h-*wrm@ZpGwwSDowSxnDIKSq8u(Z%O>A&Sg+WzO|y2! z?(TXxSNB(QUZ~KtwZG^L%))8UXp=~KV8qR4eGp8+(d!=3i|fL>w^0os{53JkhB_du zSuf^q)GX0cXKmkF`lzh4H43-Rnwl?6n^-Ey`(B3J~ zv$3%yW_mu2c)WTN#Av=%NWZqOy-DBx^%F8`mA02?1S3a{VoffJhrzyh{-=<6!9tue zw*BtnR20}LcMGJLmibBjQwe9>-NQ5Da@%p!J~)r*T@+UQGhZ|8hHtmfZHgw-dy^tp zj8P*h)QM5leyf(Ppo$-PW+|@E^GdH6UOb%OrAL0I86Ef-cMBwJqtMXT2|Rh^v$;(C z@EvMqrO``R7JOC;y4oK5A{X6-TamM&E427Msg|v`N813sM5(VslNe(-*Js& z#2rJs!;-G$LOIrEi7dHOG{(J8gl|!5a7_#;=Q(=dd@)Zx(P(0O86d|KC^9Dnw@e3{gZ1t1djpS16kxu#sV1J%PPJ>AH zi}t|OrlwkA;r6o2>48U+;CfgG4o1}xU(zCg8SU(;gqnp@-N^0R;B=)aK|Q2x>O1r` zdht1}Bh%%S8RqVkun3oIk8ixE^QV2>@4U{;U~a~v@v#t1qD*ZQ>1}nkoJ%kYhF7>< z@g|L;p)~yiF}Cuesa%T}7RLC87%COyH$jer6LZwY1=b!Tz_cN(lKc9p4mT@zj{O;j z=LO^6CESiV*)C~9KMkOdv*eA17f)|R_eO(~bT6(M)9+VF+ZP(hqa7LXUHB-12^{>E8Nc)6_+@4UbjPD0hk;hp5sem@- z(I4{WD>iT)rh(e8yV^2}y0s`yzFGqhziG@iykz^uSn}2E9$b7ZeC}Nbc9>}t=7r~p zgU+zX&rIt`D0T44x93Lb%iPsABu+bH{1Ka- zKv>R^PRRFEL(Dk*A^ueN`=zMo-B25lY0sxusjR25r9yh;0;8ej)Pa`4K>;4)^!!=q z&NG%G=3jxC@h-X9B>U8Ki{|}|k&Ove!Xo8qm-L_ejG-a(n@y;H;DB!18c?0uDXs!KhK!=D8*dQT2pXMkPNxwDB1Su|`uJLZkg)+mHz#(NiI`z4bR zyudYcf&v3?e6dC1e&vt8qqbg~#ayglbndmzr1F4H1x$=_cHS35%EI*uVfrQbfXqok zw5TAcdG~06n5d(VMZkSHZ5zA^()`^yFiP+45!G}l`EljBfu z=l%MT0mk@mj2^GN(;plt(-;21r?1USzPa!}d$K&BOwd>OBXI&aHH0i6pxoQP+b`Q% zPQPt>%|wy!WUK-pxiC4#`Po%!hX0cy)bQsxX`2Z4YLoha`3k|;!Vh_MH%z^Q;{(R% ztO92VM}rRy3cHJsaRdU295~}2SVav)&~Yk@;6Vcf4!2z}z0H7?d%si1GKaX<6We(t zoa}7(GkXI~6+NrayoDI9N?GA;17R4QOPT3w`4QHk{j^UsZ3#qqdNqN&x@^0Akqh-C zb15}>Yx*3PcOMvjM4H`>%cn_`Keta0&D%v?Ax)Te!`6mhO8iz24KO{xM2Y zfjaWW`4z;^0<)DLH^g_`hcaEgnUbd4;2?WFgj&qUY=59}*Mh@BaYKI8eii+-!Q8W> zA^cL7PKHMRZL$j4Vr>^Jquy?t&zuJg+bBSW- z#>!|)Y~h&Tj=aTs0^=dj@85AxCcJZe8k90Pp*|J`9q?T(VX${sggkpp5bXPbF|3B; zlj-t|1W|C&s5x2ahx;r|iOcu-yMbOfyKw(P%I@;Qh87f{9N?Yvr zF^QH|b>>s6u1>D!lU@2o;}6nT2f9yCCn!SFu-6(FD|EYP$@h?<0GnGU49O_Usgo$o z6V8PG=@T87?JceY)qy#V%&OR2^?vBT&1EKRqS8N4Nr>~*_%=B;KF%g_f>B0=ba|>kufxQ2T zATs176A!sl-ez!&;X@*?p$MJrRU$8``q@oR87hkd4hNp~zlgR-$wBm^Qi#enJn%mN zl>;!rmM{x~5r$N?o4!u&gadxB>k;|%kHx#Bj?un-wWg;gGcQ^sY-%;6OB+#yi%}7p z9_Cv5V{={BS zX{Ei{b#2IZ<3~_0{&xWW1u80^ zjv_z>fLrHp9KS$H`v;D98~i(Z+Mz&54hH;<#WVu3C+^_r#<1f8^oAl-?4CH4tmUv?)#9R67v_EvLuTB(W(fLY)Rf*k+Lefb|;=2#JU*d@z7 z3J4iZgK8tpj;boQ!~ij!3_3)9_Wc#%$)0g^FZJmnA;d6<{XGna4i(+K5E$#6llni9 z8RoN}ALahDVbq4LRt6$T%gBlHvmqNEV->F(AcPF_bPpo^X|S*%`Gj%z$U;s=+gEqH zj#wHtv!>lpJRP$mTN$cIFv0!)&Rz5?e1IO5EbnHLXDT}+W7^gciHBz!`Aiw~h#Zeo z0}yW>zqvoT4#8dl?+Xo4r$4MGX&uf zqI=qW^x>H?cDD%YK8A$#^pvPJ@<$|l?Hb&2jXw+|)RAYY@@$#^+cDzcsz79RzrmkS z(P|oKZWdhmR1pCF5p6*(U{gXi@~7oOiw>L%RO6pR=(otJ(zzDxZh+3USZ8-`YBp z$)onT%z5(<_lS)^!P9jRi|*2FxK&$Vdiy5V+t;Jk?2i5`c#X@98_jHGWkd~gb9p+y zWdNe8a0+~g;$D)1Dm3382!lu<&rE-R%rJAJY1abDtu`TdiGm4V1g!)gdIj$V_)qqY zpXZMWH}(LH#jdXFK9h8A$v{sil=9jesB$qpB}ur8zQ%sk@#7(vIKB_jkrb0kdqF7{ zT5}k7O;}a;g_8)wtw;tktnpipUUy-fxcwdb;tWyIqsH-!X1RNW%A?-8x~ECsk$c%x zWFp*fN^FaICpJXXP)*I2pZ@P@`a9k#gE$WguZ{DCI8viFAUA6X^xCJ7k^X5{pvV)k zIY4)8$hQ&Q*A3E?JaX|2wQda!f1NEP#;^g!~;Dd;wE z=DS869UBt(>j!AYDK8(=S&(u>!GkdAb$PLSTZyFFnFDHqEkL@*=Rnw9)~iTQhT;*e zx3e>*X-l>+O2L-x$@m4%6>eFG#_QfXx|Q%1KZsnJ$TZcD{U*p0*|IlO3HO=tw71Lw z{Oo%1-L*0b=Glvpu#F9XKn}5E@6THnUK(ynBL(hY$AE-n zem?q4=jfR*Bgyrrg!jLGxeGk%5aDp!OR?&@YVQJFkjdV>8J<=lvjWa8qGV|a$NCRZ z9iV#q$06$ye1Ec&6_5^UAwR85V_EKL`n-h?+KKGUtrL2`hhoOf zi^X?y#;VR^pWfMMb$74m7@%KxJ<|wqaEiOqBIG{1R5Yypo@*G+{WVB3M+eY}bqU{a z{!qSPx4Z33bK86rxMp@UV=}FNmfWns5Cn6mp@c4xZ!&)o)3pGx5Te- zEc3OmihW+CJ+BYVv!&uNP=DGn2xK0U{~NAoK8 z>|6d_4<`0`nbAVpZ$ngisHd;p^O)5uO|zz(lI~0tn`JOeYZ}N?fnSA(03ur z;>WpEXGX>J$%q{nHb6NHC^8U%&5uOMO^ioexXk@1H}S4fww|3-vb`d44U#muKhm{1 z<-pBK5U&p-TtB^G(Y66_Y!%uh* zzf5v8L7AmmKU03?jJdY86y{ZTnaM7%!NyJ}M(dn;Chk-WMNz_V_$4LlN0lxOvCYf zHf8YU=_9k)M$U*g8{R%T#W+@tVjRRd8FGjJk~lZ(#bOrIzZLHQ#Fj2x1oT7S^Mr$R za|!Qg++*D!26h2BzFs=Te{Hf$BSyA_;C!3Z^V-=s6t zO8yq{MP_$tj<6T@YTi%shI3C>>IQD2)51e-|kVs z#JKaf5Tb(L?11PjOfpj~GeC3`_=hR zSk!sI+hQ6`AiC|S|3<Ee>o+Htn||2hJx0q21`} zUOB*DylQ|9q{m-!Y&bz6Sy9}+PW!StqW_?&7E6Mg{t{3F9~CBwz`7>T z5dZkTvKG4*_7ChHaR|pW*aH9G>vi0lh2Vs!x