PRL-LIB-DUMP-V4.0.10
(|root_2_irrat_begin| COM NIL ((|!text| ("************ ROOT_2_IRRAT ************" . |string|))) NIL NIL)

(|qrat_irreduc_witness_orig| THM NIL ((|all|) (NIL (|qrat|)) (("u") (|squash|) (NIL (|exists|) (NIL (|int|)) (("n") (|exists|) (NIL (|int_nzero|)) (("d") (|and|) (NIL (|equal|) (NIL (|qrat|)) (NIL . "u") (NIL (|numq|) (NIL . "n") (NIL . "d"))) (NIL (|coprime|) (NIL . "n") (NIL . "d"))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("D 0 THENM InstLemma `qrat_witness` [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL . "u")) (NIL (|!text| ("]" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 2 THENM D 0 THENM ExRepD" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!text_cons|) (NIL (|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|nequal|) (NIL (|int|)) (NIL (|gcd|) (NIL . "n") (NIL . "d")) (NIL (|natural_number| ("0" . |natural|))))) (NIL (|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("THENM Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|nequal|) (NIL (|int|)) (NIL (|divide|) (NIL . "d") (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|natural_number| ("0" . |natural|))))) (NIL (|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM " . |string|))))))))))) (NIL (|!text_cons|) (NIL (|!text| ("Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|divide|) (NIL . "n") (NIL (|gcd|) (NIL . "n") (NIL . "d")))) (NIL (|!text_cons|) (NIL (|!text| (";" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|divide|) (NIL . "d") (NIL (|gcd|) (NIL . "n") (NIL . "d")))) (NIL (|!text| ("] 0" . |string|)))))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("Sel (-1) (FLemma `gcd_zero_result` [5])" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!text| ("Auto" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `div_zero_a`" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!text| ("Auto" . |string|)))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_is_divisor_2`" . |string|)))) (NIL (|!text| ("" . |string|))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("RWH (RevLemmaWithC [`n'," . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|!text| ("] `numq_factor_cancel`) 0" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWH (LemmaC `mul_com`) 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("RemoveLabel THENM EqTypeCD" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THEN Try (Complete Auto)" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("BLemma `int_entire_a`" . |string|)))) (NIL (|!text| ("" . |string|))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWH (GenLemmaC 1 `divides_iff_div_exact`) 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_is_divisor_1`" . |string|)))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_is_divisor_2`" . |string|)))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("RemoveLabel THEN EqTypeCD" . |string|)))) (NIL (|!text| ("" . |string|)))))) (((|!text| ("Auto" . |string|))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("Unfold `coprime` 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("Using [`n'," . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|!text| ("] (BLemma `gcd_p_mul_elim`) " . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("RWH IntSimpC 0" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWH (GenLemmaC 1 `divides_iff_div_exact`) 0" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_is_divisor_1`" . |string|)))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_is_divisor_2`" . |string|)))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `gcd_sat_gcd_p`" . |string|)))) (NIL (|!text| ("" . |string|)))))))))))) ((|lambda|) (("u") (|apply|) (NIL (|lambda|) (("%1") (|apply|) (NIL (|lambda|) (("%1") (|axiom|))) (NIL (|apply|) (NIL . "%1") (NIL . "u")))) (NIL (|qrat_witness| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))) (REFS (|gcd_sat_gcd_p| |comb_for_gcd_p_wf| |gcd_p_mul_elim| |coprime| |gcd_is_divisor_1| |divides_iff_div_exact| |int_entire_a| |auto| |label| |mul_com| |comb_for_numq_wf| |numq_factor_cancel| |rev_implies| |iff| |gcd_is_divisor_2| |div_zero_a| |gcd_zero_result| |int_nzero_wf| |coprime_wf| |numq_wf| |nequal_wf| |subtype| |gcd_wf| |divide_wfa| |int_nzero| |implies| |false| |not| |nequal| |prop| |and| |inewline| |exists| |true| |squash| |qrat_wf| |qrat_witness| |member| |all| |iprl_term| |aux_auto| |itext_cons| |iml_text_cons|) (|gcd_sat_gcd_p| |comb_for_gcd_p_wf| |gcd_p_mul_elim| |gcd_is_divisor_1| |divides_iff_div_exact| |int_entire_a| |mul_com| |comb_for_numq_wf| |numq_factor_cancel| |gcd_is_divisor_2| |div_zero_a| |gcd_zero_result| |qrat_witness|))) NIL)

(|qrat_irreduc_witness| THM NIL ((|all|) (NIL (|qrat|)) (("u") (|squash|) (NIL (|exists|) (NIL (|int|)) (("n") (|exists|) (NIL (|int_nzero|)) (("d") (|and|) (NIL (|equal|) (NIL (|qrat|)) (NIL . "u") (NIL (|numq|) (NIL . "n") (NIL . "d"))) (NIL (|coprime|) (NIL . "n") (NIL . "d"))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("D 0 THENM InstLemma `qrat_witness` [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL . "u")) (NIL (|!text_cons|) (NIL (|!text| ("]" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM D 2 THENM D 0 THENM ExRepD" . |string|)))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("% Facts to help type-checking %" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("(Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|nequal|) (NIL (|int|)) (NIL (|gcd|) (NIL . "n") (NIL . "d")) (NIL (|natural_number| ("0" . |natural|))))) (NIL (|!ml_text_cons|) (NIL (|!text| (" THENA" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("  " . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("D 0 THENM Sel (-1) (FLemma `gcd_zero_result` [5])" . |string|)))) (NIL (|!ml_text_cons|) (NIL (|!text| (")" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("THEN " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("(Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|nequal|) (NIL (|int|)) (NIL (|divide|) (NIL . "d") (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|natural_number| ("0" . |natural|))))) (NIL (|!ml_text_cons|) (NIL (|!text| (" THENA" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("  " . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("Backchain ``div_zero_a gcd_is_divisor_2``" . |string|)))) (NIL (|!ml_text_cons|) (NIL (|!text| (")" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("" . |string|))))))))))))))))))))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|divide|) (NIL . "n") (NIL (|gcd|) (NIL . "n") (NIL . "d")))) (NIL (|!text_cons|) (NIL (|!text| (";" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|divide|) (NIL . "d") (NIL (|gcd|) (NIL . "n") (NIL . "d")))) (NIL (|!text| ("] 0" . |string|)))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("RWH (RevLemmaWithC [`n'," . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|!text| ("] `numq_factor_cancel`) 0" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!text_cons|) (NIL (|!text| ("RWH (LemmaC `mul_com`) 0 " . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWH (GenLemmaC 1 `divides_iff_div_exact`) 0" . |string|))))) (NIL (|!ml_text_cons|) (NIL (|!text| (" " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("THENA Repeat " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("  (Progress Auto" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("   ORELSE (RemoveLabel THEN EqTypeCD)" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("   ORELSE Backchain ``gcd_is_divisor_1 gcd_is_divisor_2 int_entire_a``)" . |string|))))))))))))) (((|!text| ("Auto" . |string|)))))) (((|!text| ("Unfold `coprime` 0" . |string|))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("Using [`n'," . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|gcd|) (NIL . "n") (NIL . "d"))) (NIL (|!text_cons|) (NIL (|!text| ("] (BLemma `gcd_p_mul_elim`)" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWH IntSimpC 0 " . |string|)))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text_cons|) (NIL (|!text| ("RWH (GenLemmaC 1 `divides_iff_div_exact`) 0" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THEN Backchain ``gcd_is_divisor_1 gcd_is_divisor_2 gcd_sat_gcd_p``" . |string|)))))) (NIL (|!text| ("" . |string|))))))))))) ((|lambda|) (("u") (|apply|) (NIL (|lambda|) (("%1") (|apply|) (NIL (|lambda|) (("%1") (|axiom|))) (NIL (|apply|) (NIL . "%1") (NIL . "u")))) (NIL (|qrat_witness| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))) (REFS (|gcd_sat_gcd_p| |comb_for_gcd_p_wf| |gcd_p_mul_elim| |coprime| |gcd_is_divisor_1| |gcd| |int_entire_a| |divides_iff_div_exact| |label| |mul_com| |comb_for_numq_wf| |numq_factor_cancel| |rev_implies| |iff| |int_nzero_wf| |coprime_wf| |numq_wf| |divide_wfa| |nequal_wf| |gcd_is_divisor_2| |div_zero_a| |gcd_wf| |false| |int_nzero| |subtype| |and| |gcd_zero_result| |prop| |implies| |not| |nequal| |auto| |qrat_wf| |exists| |true| |squash| |qrat_witness| |member| |all| |iprl_term| |aux_auto| |inewline| |itext_cons| |iml_text_cons|) (|gcd_sat_gcd_p| |comb_for_gcd_p_wf| |gcd_p_mul_elim| |gcd_is_divisor_1| |divides_iff_div_exact| |int_entire_a| |mul_com| |comb_for_numq_wf| |numq_factor_cancel| |gcd_is_divisor_2| |div_zero_a| |gcd_zero_result| |qrat_witness|))) NIL)

(|exists_zero_one_elim| THM NIL ((|all|) (NIL (|function|) (NIL (|int_seg|) (NIL (|natural_number| ("0" . |natural|))) (NIL (|natural_number| ("2" . |natural|)))) (("") (|prop| (NUPRL-PARAMETER-VARS::|i| . |level-expression|)))) (("P") (|iff|) (NIL (|exists|) (NIL (|int_seg|) (NIL (|natural_number| ("0" . |natural|))) (NIL (|natural_number| ("2" . |natural|)))) (("i") (|so_apply|) (NIL . "P") (NIL . "i"))) (NIL (|or|) (NIL (|so_apply|) (NIL . "P") (NIL (|natural_number| ("0" . |natural|)))) (NIL (|so_apply|) (NIL . "P") (NIL (|natural_number| ("1" . |natural|))))))) (COMPLETE (((|!text| ("GenExRepD THENA Auto" . |string|))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|or|) (NIL (|equal|) (NIL (|int_seg|) (NIL (|natural_number| ("0" . |natural|))) (NIL (|natural_number| ("2" . |natural|)))) (NIL . "i") (NIL (|natural_number| ("0" . |natural|)))) (NIL (|equal|) (NIL (|int_seg|) (NIL (|natural_number| ("0" . |natural|))) (NIL (|natural_number| ("2" . |natural|)))) (NIL . "i") (NIL (|natural_number| ("1" . |natural|)))))) (NIL (|!text| ("" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!text| ("SIAuto" . |string|)))) (((|!text| ("D 4" . |string|))) (((|!text| ("HypSubst 4 3 THENA Auto" . |string|))) (((|!text| ("ProveProp THENA Auto" . |string|))))) (((|!text| ("HypSubst 4 3 THENA Auto" . |string|))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("ProveProp" . |string|)))) (NIL (|!text| ("" . |string|))))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text_cons|) (NIL (|!text| ("Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|natural_number| ("0" . |natural|)))) (NIL (|!text| ("] 0" . |string|)))))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text_cons|) (NIL (|!text| ("Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|natural_number| ("1" . |natural|)))) (NIL (|!text| ("] 0" . |string|)))))) (NIL (|!text| ("" . |string|))))))) ((|lambda|) (("P") (|pair|) (NIL (|lambda|) (("%") (|spread|) (NIL . "%") (("i" "%1") (|apply|) (NIL (|lambda|) (("%2") (|decide|) (NIL . "%2") (("%") (|apply|) (NIL (|lambda|) (("%2") (|inl|) (NIL . "%2"))) (NIL . "%1")) (("%3") (|apply|) (NIL (|lambda|) (("%4") (|inr|) (NIL . "%4"))) (NIL . "%1")))) (NIL (|ifthenelse|) (NIL (|eq_int|) (NIL . "i") (NIL (|natural_number| ("0" . |natural|)))) (NIL (|axiom|)) (NIL (|axiom|)))))) (NIL (|lambda|) (("%") (|decide|) (NIL . "%") (("%1") (|pair|) (NIL (|natural_number| ("0" . |natural|))) (NIL . "%1")) (("%2") (|pair|) (NIL (|natural_number| ("1" . |natural|))) (NIL . "%2")))))) (REFS (|auto| |iprl_term| |aux_auto| |itext_cons| |iml_text_cons| |le_wf| |false| |not| |le| |lelt| |int_seg| |subtype| |int_seg_wf| |rev_implies| |or| |so_apply1| |exists| |implies| |and| |iff| |member| |prop| |all|) NIL)) NIL)

(|two_div_square| THM NIL ((|all|) (NIL (|int|)) (("n") (|implies|) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|multiply|) (NIL . "n") (NIL . "n"))) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "n")))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|implies|) (NIL (|eqmod|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|multiply|) (NIL . "n") (NIL . "n")) (NIL (|natural_number| ("0" . |natural|)))) (NIL (|eqmod|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "n") (NIL (|natural_number| ("0" . |natural|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!text_cons|) (NIL (|!ml_text_cons|) (NIL (|!text| ("InstLemma `eqmod_exists` [" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|natural_number| ("2" . |natural|)))) (NIL (|!ml_text_cons|) (NIL (|!text| (";" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL . "n")) (NIL (|!text| ("]" . |string|))))))) (NIL (|!text| ("" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWH (LemmaC `exists_zero_one_elim`) 3" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!text| ("D 3 THEN Auto" . |string|))) (((|!text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!text_cons|) (NIL (|!ml_text_cons|) (NIL (|!text| ("FLemma `multiply_functionality_wrt_eqmod` [3;3]" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM ArithSimp 4" . |string|))))) (NIL (|!text| ("" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("FLemma `eqmod_unique` [2;4]" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!text| ("Auto" . |string|)))))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|siauto|) (NIL (|!text| ("Unfold `eqmod` 2 THEN ArithSimp 2" . |string|)))) (NIL (|!text| ("" . |string|)))))))) ((|lambda|) (("n") (|apply|) (NIL (|lambda|) (("%1") . "%1")) (NIL (|lambda|) (("%") (|apply|) (NIL (|lambda|) (("%1") (|apply|) (NIL (|lambda|) (("%4") (|apply|) (NIL (|lambda|) (("%6") (|decide|) (NIL . "%6") (("%7") . "%7") (("%8") (|apply|) (NIL (|lambda|) (("%9") (|apply|) (NIL (|lambda|) (("%17") (|apply|) (NIL (|lambda|) (("%18") (|apply|) (NIL (|lambda|) (("%25") (|axiom|))) (NIL (|axiom|)))) (NIL (|eqmod_unique| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL . "%9") (NIL (|natural_number| ("2" . |natural|)))) (NIL . "n")) (NIL (|natural_number| ("1" . |natural|)))) (NIL . "n")) (NIL (|natural_number| ("1" . |natural|)))) (NIL . "%8")) (NIL . "%8")))) (NIL (|multiply_functionality_wrt_eqmod| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|)))))) (NIL (|apply|) (NIL . "%4") (NIL (|apply|) (NIL (|apply|) (NIL . "%1") (NIL (|natural_number| ("2" . |natural|)))) (NIL . "n"))))) (NIL (|apply|) (NIL (|lambda|) (("%4") (|spread|) (NIL . "%4") (("%5" "%6") . "%5"))) (NIL (|apply|) (NIL (|lambda|) (("%4") (|apply|) (NIL . "%4") (NIL (|so_lambda|) (("b") (|eqmod|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "n") (NIL . "b"))))) (NIL (|exists_zero_one_elim| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|) (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (NIL (|eqmod_exists| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (REFS EMPTY (|comb_for_divides_wf| |eqmod_unique| |comb_for_eqmod_wf| |multiply_functionality_wrt_eqmod| |exists_zero_one_elim| |eqmod_exists|))) NIL)

(|root_2_irrat_over_int_orig| THM NIL ((|not|) (NIL (|exists|) (NIL (|int|)) (("m") (|exists|) (NIL (|int|)) (("n") (|and|) (NIL (|coprime|) (NIL . "m") (NIL . "n")) (NIL (|equal|) (NIL (|int|)) (NIL (|multiply|) (NIL . "m") (NIL . "m")) (NIL (|multiply|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|multiply|) (NIL . "n") (NIL . "n")))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0 THENM ExRepD" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "m"))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `two_div_square`" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!text| ("Unfold `divides` 0" . |string|))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text_cons|) (NIL (|!text| ("Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|multiply|) (NIL . "n") (NIL . "n"))) (NIL (|!text| ("] 0" . |string|)))))) (NIL (|!text| ("" . |string|)))))))) (((|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "n"))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("BLemma `two_div_square`" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("All (Unfold `divides`)" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THEN ExRepD" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|siauto|) (NIL (|!text_cons|) (NIL (|!text| ("With " . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|multiply|) (NIL . "c") (NIL . "c"))) (NIL (|!text| (" (D 0)" . |string|)))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|siauto|) (NIL (|!text| ("RWW \"6\" 4" . |string|)))) (NIL (|!text| ("" . |string|))))))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWO \"coprime_elim\" 3" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("FHyp 3 [5;6]" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text_cons|) (NIL (|!text| ("RWW \"assoced_elim\" 7" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM D (-1)" . |string|)))))) (NIL (|!text| ("" . |string|))))))))))) ((|lambda|) (("%") (|spread|) (NIL . "%") (("m" "%1") (|spread|) (NIL . "%1") (("n" "%2") (|spread|) (NIL . "%2") (("%3" "%4") (|apply|) (NIL (|lambda|) (("%5") (|apply|) (NIL (|lambda|) (("%6") (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|lambda|) (("%8") (|apply|) (NIL (|lambda|) (("%8") (|apply|) (NIL (|lambda|) (("%9") (|apply|) (NIL (|lambda|) (("%9") (|decide|) (NIL . "%9") (("%") (|axiom|)) (("%10") (|axiom|)))) (NIL (|apply|) (NIL . "%9") (NIL . "%8")))) (NIL (|apply|) (NIL (|lambda|) (("%9") (|spread|) (NIL . "%9") (("%10" "%11") . "%10"))) (NIL (|apply|) (NIL (|lambda|) (("%9") (|apply|) (NIL (|apply|) (NIL . "%9") (NIL (|natural_number| ("2" . |natural|)))) (NIL (|natural_number| ("1" . |natural|))))) (NIL (|assoced_elim| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL . "%8") (NIL (|natural_number| ("2" . |natural|)))) (NIL . "%5")) (NIL . "%6")))) (NIL . "%7"))) (NIL (|apply|) (NIL . "%7") (NIL . "%3")))) (NIL (|apply|) (NIL (|lambda|) (("%7") (|spread|) (NIL . "%7") (("%8" "%9") . "%8"))) (NIL (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|apply|) (NIL . "%7") (NIL . "m")) (NIL . "n"))) (NIL (|coprime_elim| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (NIL (|apply|) (NIL (|lambda|) (("%6") (|apply|) (NIL (|apply|) (NIL . "%6") (NIL . "n")) (NIL (|apply|) (NIL (|lambda|) (("%6") . "%6")) (NIL (|spread|) (NIL . "%5") (("c" "%6") (|pair|) (NIL (|multiply|) (NIL . "c") (NIL . "c")) (NIL (|axiom|))))))) (NIL (|two_div_square| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|)))))) (NIL (|apply|) (NIL (|lambda|) (("%5") (|apply|) (NIL (|apply|) (NIL . "%5") (NIL . "m")) (NIL (|apply|) (NIL (|lambda|) (("%5") . "%5")) (NIL (|pair|) (NIL (|multiply|) (NIL . "n") (NIL . "n")) (NIL (|axiom|)))))) (NIL (|two_div_square| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))))) (REFS (|false| |assoced_elim| |or| |coprime_elim| |rev_implies| |iff| |siauto| |inewline| |auto| |itext_cons| |divides| |two_div_square| |iprl_term| |all| |coprime_wf| |prop| |member| |and| |exists| |implies| |not| |aux_auto| |iml_text_cons|) (|assoced_elim| |coprime_elim| |two_div_square|))) NIL)

(|root_2_irrat_over_int| THM NIL ((|not|) (NIL (|exists|) (NIL (|int|)) (("m") (|exists|) (NIL (|int|)) (("n") (|and|) (NIL (|coprime|) (NIL . "m") (NIL . "n")) (NIL (|equal|) (NIL (|int|)) (NIL (|multiply|) (NIL . "m") (NIL . "m")) (NIL (|multiply|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|multiply|) (NIL . "n") (NIL . "n")))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0 THENM ExRepD" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "m"))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("BLemma `two_div_square` THENM Unfold `divides` 0" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM AutoInstConcl []" . |string|)))))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("Assert " . |string|))) (NIL (|!ml_text_cons|) (NIL (|!prl_term|) (NIL (|divides|) (NIL (|natural_number| ("2" . |natural|))) (NIL . "n"))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|siauto|) (NIL (|!text_cons|) (NIL (|!text| ("BLemma `two_div_square` THENM All (Unfold `divides`)" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text_cons|) (NIL (|!text| ("THENM ExRepD THENM Inst [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL (|multiply|) (NIL . "c") (NIL . "c"))) (NIL (|!text_cons|) (NIL (|!text| ("] 0" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWO \"6\" 4" . |string|)))))))))) (NIL (|!text| ("" . |string|)))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWO \"coprime_elim\" 3 THENM FHyp 3 [5;6]" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("RWO \"assoced_elim\" 7 THENM D (-1)" . |string|)))) (NIL (|!text| ("" . |string|)))))))))) ((|lambda|) (("%") (|spread|) (NIL . "%") (("m" "%1") (|spread|) (NIL . "%1") (("n" "%2") (|spread|) (NIL . "%2") (("%3" "%4") (|apply|) (NIL (|lambda|) (("%5") (|apply|) (NIL (|lambda|) (("%6") (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|lambda|) (("%8") (|apply|) (NIL (|lambda|) (("%8") (|apply|) (NIL (|lambda|) (("%9") (|apply|) (NIL (|lambda|) (("%9") (|decide|) (NIL . "%9") (("%") (|axiom|)) (("%10") (|axiom|)))) (NIL (|apply|) (NIL . "%9") (NIL . "%8")))) (NIL (|apply|) (NIL (|lambda|) (("%9") (|spread|) (NIL . "%9") (("%10" "%11") . "%10"))) (NIL (|apply|) (NIL (|lambda|) (("%9") (|apply|) (NIL (|apply|) (NIL . "%9") (NIL (|natural_number| ("2" . |natural|)))) (NIL (|natural_number| ("1" . |natural|))))) (NIL (|assoced_elim| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (NIL (|apply|) (NIL (|apply|) (NIL (|apply|) (NIL . "%8") (NIL (|natural_number| ("2" . |natural|)))) (NIL . "%5")) (NIL . "%6")))) (NIL . "%7"))) (NIL (|apply|) (NIL . "%7") (NIL . "%3")))) (NIL (|apply|) (NIL (|lambda|) (("%7") (|spread|) (NIL . "%7") (("%8" "%9") . "%8"))) (NIL (|apply|) (NIL (|lambda|) (("%7") (|apply|) (NIL (|apply|) (NIL . "%7") (NIL . "m")) (NIL . "n"))) (NIL (|coprime_elim| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))) (NIL (|apply|) (NIL (|lambda|) (("%6") (|apply|) (NIL (|apply|) (NIL . "%6") (NIL . "n")) (NIL (|apply|) (NIL (|lambda|) (("%6") . "%6")) (NIL (|spread|) (NIL . "%5") (("c" "%6") (|pair|) (NIL (|multiply|) (NIL . "c") (NIL . "c")) (NIL (|axiom|))))))) (NIL (|two_div_square| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|)))))) (NIL (|apply|) (NIL (|lambda|) (("%5") (|apply|) (NIL (|apply|) (NIL . "%5") (NIL . "m")) (NIL (|apply|) (NIL (|lambda|) (("%5") . "%5")) (NIL (|pair|) (NIL (|multiply|) (NIL . "n") (NIL . "n")) (NIL (|axiom|)))))) (NIL (|two_div_square| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|))))))))) (REFS EMPTY (|assoced_elim| |coprime_elim| |two_div_square|))) NIL)

(|root_2_irrat_orig| THM NIL ((|not|) (NIL (|exists|) (NIL (|qrat|)) (("u") (|equal|) (NIL (|qrat|)) (NIL (|mulq|) (NIL . "u") (NIL . "u")) (NIL (|numq|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|natural_number| ("1" . |natural|))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0 THENM D (-1)" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("InstLemma `qrat_irreduc_witness` [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL . "u")) (NIL (|!text_cons|) (NIL (|!text| ("]" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text_cons|) (NIL (|!text| ("THENM D (-1)" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM ExRepD" . |string|)))))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWW \"5\" 2" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("Unfolds ``mulq numq`` 6" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM AbReduce 6" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWW \"eq_qrat_elim\" 6" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("Unfolds ``qmul qequiv`` 6" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("THENM AbReduce 6" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!ml_text_cons|) (NIL (|!text| ("THENM " . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("RWH IntSimpC 6" . |string|)))) (NIL (|!text| ("" . |string|))))))))) (((|!ml_text_cons|) (NIL (|!text| ("AssertLemma `root_2_irrat_over_int` []" . |string|))) (NIL (|!ml_text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM (D (-1))" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("AutoInstConcl [5]" . |string|)))) (NIL (|!text| ("" . |string|))))))))))))) ((|lambda|) (("%") (|spread|) (NIL . "%") (("u" "%1") (|apply|) (NIL (|lambda|) (("%2") (|apply|) (NIL (|lambda|) (("%2") (|axiom|))) (NIL (|apply|) (NIL . "%2") (NIL . "u")))) (NIL (|qrat_irreduc_witness| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|)))))) (REFS (|coprime_wf| |auto| |root_2_irrat_over_int| |qnum| |pi2| |pi1| |qdenom| |qnumer| |qequiv| |qmul| |qnum_wf| |qmul_wf| |eq_qrat_elim| |quot_inj| |qrat_inj| |quot_let| |qrat_proj| |mulq| |numq| |true| |comb_for_mulq_wf| |rev_implies| |iff| |and| |squash| |qrat_irreduc_witness| |iprl_term| |inewline| |itext_cons| |nequal_wf| |false| |nequal| |int_nzero| |subtype| |numq_wf| |all| |mulq_wf| |qrat_wf| |prop| |member| |exists| |implies| |not| |aux_auto| |iml_text_cons|) (|root_2_irrat_over_int| |eq_qrat_elim| |comb_for_mulq_wf| |qrat_irreduc_witness|))) NIL)

(|root_2_irrat| THM NIL ((|not|) (NIL (|exists|) (NIL (|qrat|)) (("u") (|equal|) (NIL (|qrat|)) (NIL (|mulq|) (NIL . "u") (NIL . "u")) (NIL (|numq|) (NIL (|natural_number| ("2" . |natural|))) (NIL (|natural_number| ("1" . |natural|))))))) (COMPLETE (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text| ("D 0 THENM D (-1)" . |string|)))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("InstLemma `qrat_irreduc_witness` [" . |string|))) (NIL (|!text_cons|) (NIL (|!prl_term|) (NIL . "u")) (NIL (|!text_cons|) (NIL (|!text| ("]" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text_cons|) (NIL (|!text| ("THENM D (-1) THENM ExRepD" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWW \"5\" 2 THENM On [4;1] Thin" . |string|)))))))))) (NIL (|!text| ("" . |string|))))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|aux_auto|) (NIL (|!text_cons|) (NIL (|!text| ("Unfolds ``mulq numq`` 4 THENM AbReduce 4 " . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text_cons|) (NIL (|!text| ("THENM RWO \"eq_qrat_elim\" 4 " . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text_cons|) (NIL (|!text| ("THENM Unfolds ``qmul qequiv`` 4 THENM AbReduce 4" . |string|))) (NIL (|!text_cons|) (NIL (|!newline|)) (NIL (|!text| ("THENM RWH IntSimpC 4" . |string|)))))))))) (NIL (|!text| ("" . |string|))))) (((|!text| ("AssertLemma `root_2_irrat_over_int` [] THENM D (-1)" . |string|))) (((|!ml_text_cons|) (NIL (|!text| ("" . |string|))) (NIL (|!ml_text_cons|) (NIL (|auto|) (NIL (|!text| ("AutoInstConcl []" . |string|)))) (NIL (|!text| ("" . |string|)))))))))) ((|lambda|) (("%") (|spread|) (NIL . "%") (("u" "%1") (|apply|) (NIL (|lambda|) (("%2") (|apply|) (NIL (|lambda|) (("%2") (|axiom|))) (NIL (|apply|) (NIL . "%2") (NIL . "u")))) (NIL (|qrat_irreduc_witness| (NUPRL-PARAMETER-VARS::|\\v| . |level-expression|)))))) (REFS (|coprime_wf| |auto| |root_2_irrat_over_int| |qnum_wf| |qmul_wf| |qnum| |pi2| |pi1| |qdenom| |qnumer| |qequiv| |qmul| |eq_qrat_elim| |quot_inj| |qrat_inj| |quot_let| |qrat_proj| |mulq| |numq| |true| |comb_for_mulq_wf| |rev_implies| |iff| |and| |squash| |qrat_irreduc_witness| |iprl_term| |inewline| |itext_cons| |nequal_wf| |false| |nequal| |int_nzero| |subtype| |numq_wf| |mulq_wf| |all| |qrat_wf| |prop| |member| |exists| |implies| |not| |aux_auto| |iml_text_cons|) (|root_2_irrat_over_int| |eq_qrat_elim| |comb_for_mulq_wf| |qrat_irreduc_witness|))) NIL)

(|root_2_irrat_end| COM NIL ((|!text| ("**************************************" . |string|))) NIL NIL)