Extensibella Standard Library

All theorems are part of the extensibella:stdLib reasoning module. Then, for example, the full name of the theorem listed below as plus_integer_unique is extensibella:stdLib:plus_integer_unique.

Integer Division

• divide_integer_unique :

  forall A B Q Q',
    A / B = Q -> A / B = Q' -> Q = Q'

• divide_integer_near_total :

  forall A B,
    is_integer A -> is_integer B -> (B = 0 -> false) -> exists Q, A / B = Q

• divide_integer_is_integer :

  forall A B Q,
    is_integer A -> is_integer B -> A / B = Q -> is_integer Q

• divide_integer_1_right :

  forall A,
    is_integer A -> A / 1 = A

• divide_integer_0_right_false :

  forall A Q,
    is_integer A -> A / 0 = Q -> false

• divide_integer_related_multiply :

  forall A B C,
    is_integer A -> is_integer B -> (B = 0 -> false) -> A * B = C -> C / B = A

• modulus_integer_unique :

  forall A B R R',
    A mod B = R -> A mod B = R' -> R = R'

• modulus_integer_near_total :

  forall A B,
    is_integer A -> is_integer B -> (B = 0 -> false) -> exists R, A mod B = R

• modulus_integer_is_integer :

  forall A B R,
    is_integer A -> is_integer B -> A mod B = R -> is_integer R

• modulus_integer_1_right :

  forall A,
    is_integer A -> A mod 1 = 0

• modulus_integer_0_right_false :

  forall A R,
    is_integer A -> A mod 0 = R -> false

• modulus_integer_related_multiply :

  forall A B C,
    is_integer A -> is_integer B -> (B = 0 -> false) -> A * B = C -> C mod B = 0

Integer Comparison

• less_integer_transitive :

  forall A B C,
    A < B -> B < C -> A < C

• less_integer_not_eq :

  forall A,
    A < A -> false

• less_integer_between_false :

  forall A B C,
    1 + A = B -> A < C -> C < B -> false

• lesseq_integer_less_or_eq :

  forall A B,
    A <= B -> A < B \/ A = B

• less_integer_lesseq :

  forall A B,
    A < B -> A <= B

• less_integer_step_lesseq :

  forall A B C,
    is_integer A -> is_integer B -> B < A -> 1 + B = C -> C <= A

• is_integer_lesseq :

  forall A,
    is_integer A -> A <= A

• lesseq_integer_transitive :

  forall A B C,
    A <= B -> B <= C -> A <= C

• less_lesseq_integer_transitive :

  forall A B C,
    A < B -> B <= C -> A < C

• lesseq_less_integer_transitive :

  forall A B C,
    A <= B -> B < C -> A < C

• less_sums :

  forall N1 N2 N3 Sum1 Sum2,
    N1 + N2 = Sum1 -> N1 + N3 = Sum2 -> is_integer N1 -> N2 < N3 -> Sum1 < Sum2

• less_integer__add_positive :

  forall N1 N2 Base Sum,
    Base < N1 -> 0 <= N2 -> N1 + N2 = Sum -> Base < Sum

• lesseq_integer__add_positive :

  forall N1 N2 Base Sum,
    Base <= N1 -> 0 <= N2 -> N1 + N2 = Sum -> Base <= Sum

• less_integer__subtract_positive :

  forall N1 N2 Base Res,
    is_integer N1 -> is_integer N2 -> N1 < Base -> 0 <= N2 -> N1 - N2 = Res -> Res < Base

• minus_integer_diff_neg :

  forall A B Diff,
    Diff < 0 -> A - B = Diff -> A < B

• minus_larger :

  forall A B Diff B' Diff',
    is_integer A -> A - B = Diff -> A - B' = Diff' -> B < B' -> Diff' < Diff

• minus_smaller_positive :

  forall A B Diff,
    A - B = Diff -> B < A -> 0 < Diff

• less_lesseq_plus_one :

  forall A B Sum,
    is_integer A -> is_integer B -> A < B -> A + 1 = Sum -> Sum <= B

• greater_less_impossible :

  forall N1 N2,
    N1 > N2 -> N1 < N2 -> false

• greater_integer__add_positive :

  forall N1 N2 Base Sum,
    N1 > Base -> 0 <= N2 -> N1 + N2 = Sum -> Sum > Base

• greater_integer_transitive :

  forall A B C,
    A > B -> B > C -> A > C

• less_integer_flip_greater :

  forall N1 N2,
    N1 < N2 -> N2 > N1

• greater_integer_flip_less :

  forall N1 N2,
    N1 > N2 -> N2 < N1

• greater_integer_not_eq :

  forall N1,
    N1 > N1 -> false

• greater_plus_positive :

  forall N1 N2 Sum,
    is_integer N2 -> is_integer N1 -> N1 + N2 = Sum -> N2 > 0 -> Sum > N1

• lesseq_integer_or_greater :

  forall A B,
    is_integer A -> is_integer B -> A <= B \/ A > B

• integer_compare_total :

  forall A B,
    is_integer A -> is_integer B -> A <= B \/ A > B

• greater_integer_greatereq :

  forall A B,
    A > B -> A >= B

• greater_integer_step_greatereq :

  forall A B C,
    is_integer A -> is_integer B -> A > B -> 1 + B = C -> A >= C

• is_integer_greatereq :

  forall A,
    is_integer A -> A >= A

• greatereq_integer__add_positive :

  forall N1 N2 Base Sum,
    N1 >= Base -> N2 >= 0 -> N1 + N2 = Sum -> Sum >= Base

• greatereq_integer_transitive :

  forall A B C,
    A >= B -> B >= C -> A >= C

• greatereq_less_integer_false :

  forall N1 N2,
    N1 >= N2 -> N1 < N2 -> false

• less_lesseq_flip_false :

  forall N1 N2,
    N1 < N2 -> N2 <= N1 -> false

• greater_lesseq_integer_false :

  forall N1 N2,
    N1 > N2 -> N1 <= N2 -> false

• greatereq_integer_greater_or_eq :

  forall A B,
    A >= B -> A > B \/ A = B

• between_integers_is_integer :

  forall Low High X,
    is_integer Low -> is_integer High -> Low <= X -> X <= High -> is_integer X

• is_integer_related :

  forall A B,
    is_integer A -> is_integer B -> (A = B \/ A < B) \/ A > B

Integer Addition

• plus_integer_unique :

  forall N1 N2 N3 N4,
    N1 + N2 = N3 -> N1 + N2 = N4 -> N3 = N4

• plus_integer_is_integer :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 + N2 = N3 -> is_integer N3

• plus_integer_total :

  forall N1 N2,
    is_integer N1 -> is_integer N2 -> exists N3, N1 + N2 = N3

• plus_integer_comm :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 + N2 = N3 -> N2 + N1 = N3

• plus_integer_assoc :

  forall N1 N2 N3 Subtotal Total,
    is_integer N1 -> is_integer N2 -> is_integer N3 -> N1 + N2 = Subtotal -> N3 + Subtotal = Total -> exists Subtotal',
      N2 + N3 = Subtotal' /\ N1 + Subtotal' = Total

• plus_zero_right :

  forall N Sum,
    N + 0 = Sum -> Sum = N

• plus_integer_is_integer_result :

  forall N1 N2 N3,
    is_integer N3 -> N1 + N2 = N3 -> is_integer N1 /\ is_integer N2

• minus_integer_unique :

  forall N1 N2 N N',
    N1 - N2 = N -> N1 - N2 = N' -> N = N'

• minus_integer_total :

  forall N1 N2,
    is_integer N1 -> is_integer N2 -> exists N3, N1 - N2 = N3

• minus_integer_is_integer :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 - N2 = N3 -> is_integer N3

• minus_integer_same :

  forall N,
    is_integer N -> N - N = 0

• minus_integer_0 :

  forall N,
    N - 0 = N

• plus_minus_same_integer :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 + N2 = N3 -> N3 - N2 = N1

• minus_plus_same_integer :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 - N2 = N3 -> N3 + N2 = N1

• minus_integer_is_integer_result :

  forall N1 N2 N3,
    is_integer N3 -> N1 - N2 = N3 -> is_integer N1 /\ is_integer N2

• plus_integer_unique_addend :

  forall N A B Sum,
    is_integer N -> is_integer A -> is_integer B -> N + A = Sum -> N + B = Sum -> A = B

• negate_integer_unique :

  forall N A B,
    - N = A -> - N = B -> A = B

• negate_integer_total :

  forall N,
    is_integer N -> exists N', - N = N'

• negate_integer_is_integer :

  forall N -N,
    is_integer N -> - N = -N -> is_integer -N

• negate_integer_double :

  forall N -N,
    - N = -N -> - -N = N

• plus_integer_0_result :

  forall A B,
    A + B = 0 -> - A = B

• plus_integer_negation :

  forall A -A,
    is_integer A -> - A = -A -> A + -A = 0

• plus_integer_negatives :

  forall A -A B -B C -C,
    is_integer A -> is_integer B -> is_integer C -> - A = -A -> - B = -B -> - C = -C -> A + B = C -> -A + -B = -C

Integer Multiplication

• multiply_integer_unique :

  forall N1 N2 N N',
    N1 * N2 = N -> N1 * N2 = N' -> N = N'

• multiply_integer_is_integer :

  forall N1 N2 N,
    is_integer N1 -> is_integer N2 -> N1 * N2 = N -> is_integer N

• multiply_integer_total :

  forall N1 N2,
    is_integer N1 -> is_integer N2 -> exists N, N1 * N2 = N

• multiply_integer_0_right :

  forall N,
    is_integer N -> N * 0 = 0

• multiply_integer_1 :

  forall A,
    is_integer A -> 1 * A = A

• multiply_integer_1_right :

  forall A,
    is_integer A -> A * 1 = A

• multiply_integer_0_result :

  forall A B,
    is_integer A -> is_integer B -> A * B = 0 -> A = 0 \/ B = 0

• multiply_integer_-1_negate :

  forall A B,
    -1 * A = B -> - A = B

• multiply_integer_negation :

  forall A B C -A -C,
    is_integer A -> is_integer B -> - A = -A -> A * B = C -> - C = -C -> -A * B = -C

• multiply_integer_comm :

  forall N1 N2 N3,
    is_integer N1 -> is_integer N2 -> N1 * N2 = N3 -> N2 * N1 = N3

• multiply_integer_distribute_over_plus :

  forall N1 N2 AddN1N2 N3 Result,
    is_integer N1 -> is_integer N2 -> is_integer N3 -> N1 + N2 = AddN1N2 -> AddN1N2 * N3 = Result -> exists MulN1N3 MulN2N3,
      (N1 * N3 = MulN1N3 /\ N2 * N3 = MulN2N3) /\ MulN1N3 + MulN2N3 = Result

• multiply_integer_assoc :

  forall N1 N2 N3 MulN1N2 Result,
    is_integer N1 -> is_integer N2 -> is_integer N3 -> N1 * N2 = MulN1N2 -> MulN1N2 * N3 = Result -> exists MulN2N3,
      N2 * N3 = MulN2N3 /\ N1 * MulN2N3 = Result

• multiply_integer_undistribute_over_plus :

  forall N1 N2 N3 MulN1N3 MulN2N3 Result,
    is_integer N1 -> is_integer N2 -> is_integer N3 -> N1 * N3 = MulN1N3 -> N2 * N3 = MulN2N3 -> MulN1N3 + MulN2N3 = Result ->
    exists AddN1N2, N1 + N2 = AddN1N2 /\ AddN1N2 * N3 = Result

Lists

• append_nil_right [A] :

  forall (L' : list A) (L : list A),
    L ++ [] = L' -> L = L'

• append_nil_left [A] :

  forall (L' : list A) (L : list A),
    [] ++ L = L' -> L = L'

• append_unique [A] :

  forall (L2 : list A) (L3 : list A) (L3' : list A) (L1 : list A),
    L1 ++ L2 = L3 -> L1 ++ L2 = L3' -> L3 = L3'

• append_anything [A] :

  forall (L2 : list A) (L : list A) (L3 : list A) (L1 : list A),
    L1 ++ L2 = L -> exists L', L1 ++ L3 = L'

• append_associative [A] :

  forall (L2 : list A) (L3 : list A) (L12 : list A) (L123 : list A) (L1 : list A),
    L1 ++ L2 = L12 -> L12 ++ L3 = L123 -> exists L23, L2 ++ L3 = L23 /\ L1 ++ L23 = L123

• append_associative_back [A] :

  forall (L2 : list A) (L3 : list A) (L23 : list A) (L123 : list A) (L1 : list A),
    L2 ++ L3 = L23 -> L1 ++ L23 = L123 -> exists L12, L1 ++ L2 = L12 /\ L12 ++ L3 = L123

• length_is [A] :

  forall (L : list A) N,
    extensibella:stdLib:length L N -> is_integer N

• length_unique [A] :

  forall (L : list A) N1 N2,
    extensibella:stdLib:length L N1 -> extensibella:stdLib:length L N2 -> N1 = N2

• cons_length [A] :

  forall H (T : list A) N,
    extensibella:stdLib:length (H::T) N -> N > 0

• length_cons [A] :

  forall (L : list A) N,
    extensibella:stdLib:length L N -> N > 0 -> exists H T, L = H::T

• length_geq_0 [A] :

  forall (L : list A) N,
    extensibella:stdLib:length L N -> N >= 0

• append_length [A] :

  forall (L1 : list A) (L2 : list A) (L : list A) N1 N2 N,
    L1 ++ L2 = L -> extensibella:stdLib:length L1 N1 -> extensibella:stdLib:length L2 N2 -> N1 + N2 = N ->
    extensibella:stdLib:length L N

• append_neq_right [A] :

  forall (L2 : list A) (L : list A) N,
    L ++ L2 = L -> extensibella:stdLib:length L2 N -> N > 0 -> false

Strings

• is_string_append :

  forall S1 S2 S3,
    extensibella:stdLib:is_string S1 -> extensibella:stdLib:is_string S2 -> S1 ++ S2 = S3 -> extensibella:stdLib:is_string S3

• is_string_eq_or_not :

  forall S1 S2,
    extensibella:stdLib:is_string S1 -> extensibella:stdLib:is_string S2 -> S1 = S2 \/
    (S1 = S2 -> false)

• append_string_is :

  forall S1 S2 S,
    extensibella:stdLib:is_string S1 -> extensibella:stdLib:is_string S2 -> S1 ++ S2 = S -> extensibella:stdLib:is_string S

• append_string_total :

  forall S1 S2,
    extensibella:stdLib:is_string S1 -> extensibella:stdLib:is_string S2 -> exists S, S1 ++ S2 = S

• string_length_total :

  forall S,
    extensibella:stdLib:is_string S -> exists N, length S N

Bools

• is_bool_eq_or_not :

  forall B1 B2,
    extensibella:stdLib:is_bool B1 -> extensibella:stdLib:is_bool B2 -> B1 = B2 \/ (B1 = B2 -> false)

• and_bool_unique :

  forall B1 B2 B B',
    B1 && B2 = B -> B1 && B2 = B' -> B = B'

• and_bool_total :

  forall B1 B2,
    extensibella:stdLib:is_bool B1 -> extensibella:stdLib:is_bool B2 -> exists B, B1 && B2 = B

• and_bool_is_bool :

  forall B1 B2 B3,
    extensibella:stdLib:is_bool B1 -> extensibella:stdLib:is_bool B2 -> B1 && B2 = B3 -> extensibella:stdLib:is_bool B3

• and_bool_comm :

  forall B1 B2 B3,
    B1 && B2 = B3 -> B2 && B1 = B3

• and_bool_true_left :

  forall B,
    extensibella:stdLib:is_bool B -> true && B = B

• and_bool_true_left_eq :

  forall B B',
    true && B = B' -> B' = B

• and_bool_true_right :

  forall B,
    extensibella:stdLib:is_bool B -> B && true = B

• and_bool_true_right_eq :

  forall B B',
    B && true = B' -> B' = B

• and_bool_false_left :

  forall B B',
    false && B = B' -> B' = false

• and_bool_false_right :

  forall B B',
    B && false = B' -> B' = false

• and_bool_associative :

  forall B1 B2 B3 BRes1 Result,
    extensibella:stdLib:is_bool B2 -> extensibella:stdLib:is_bool B3 -> B1 && B2 = BRes1 -> BRes1 && B3 = Result ->
    exists BRes2, B2 && B3 = BRes2 /\ B1 && BRes2 = Result

• and_bool_idempotent :

  forall B,
    extensibella:stdLib:is_bool B -> B && B = B

• or_bool_unique :

  forall B1 B2 B B',
    B1 || B2 = B -> B1 || B2 = B' -> B = B'

• or_bool_total :

  forall B1 B2,
    extensibella:stdLib:is_bool B1 -> extensibella:stdLib:is_bool B2 -> exists B, B1 || B2 = B

• or_bool_is_bool :

  forall B1 B2 B3,
    extensibella:stdLib:is_bool B1 -> extensibella:stdLib:is_bool B2 -> B1 || B2 = B3 -> extensibella:stdLib:is_bool B3

• or_bool_comm :

  forall B1 B2 B3,
    B1 || B2 = B3 -> B2 || B1 = B3

• or_bool_true_left :

  forall B B',
    true || B = B' -> B' = true

• or_bool_true_right :

  forall B B',
    B || true = B' -> B' = true

• or_bool_false_left :

  forall B,
    extensibella:stdLib:is_bool B -> false || B = B

• or_bool_false_left_eq :

  forall B B',
    false || B = B' -> B' = B

• or_bool_false_right :

  forall B,
    extensibella:stdLib:is_bool B -> B || false = B

• or_bool_false_right_eq :

  forall B B',
    B || false = B' -> B' = B

• or_bool_associative :

  forall B1 B2 B3 BRes1 Result,
    extensibella:stdLib:is_bool B2 -> extensibella:stdLib:is_bool B3 -> B1 || B2 = BRes1 -> BRes1 || B3 = Result ->
    exists BRes2, B2 || B3 = BRes2 /\ B1 || BRes2 = Result

• or_bool_idempotent :

  forall B,
    extensibella:stdLib:is_bool B -> B || B = B

• not_bool_unique :

  forall B1 B B',
    ! B1 = B -> ! B1 = B' -> B = B'

• not_bool_total :

  forall B,
    extensibella:stdLib:is_bool B -> exists B', ! B = B'

• not_bool_is_bool :

  forall B B',
    ! B = B' -> extensibella:stdLib:is_bool B'

• not_bool_double_negation :

  forall B B',
    ! B = B' -> ! B' = B

• and_bool_complementation :

  forall B NotB,
    ! B = NotB -> B && NotB = false

• or_bool_complementation :

  forall B NotB,
    ! B = NotB -> B || NotB = true

• and_bool__distribute_over__or :

  forall A B C OrBC Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> extensibella:stdLib:is_bool C ->
    B || C = OrBC -> A && OrBC = Result -> exists AndAB AndAC,
      (A && B = AndAB /\ A && C = AndAC) /\ AndAB || AndAC = Result

• and_bool__undistribute_over__or :

  forall A B C AndAB AndAC Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> extensibella:stdLib:is_bool C ->
    A && B = AndAB -> A && C = AndAC -> AndAB || AndAC = Result -> exists OrBC,
      B || C = OrBC /\ A && OrBC = Result

• or_bool__distribute_over__and :

  forall A B C AndBC Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> extensibella:stdLib:is_bool C ->
    B && C = AndBC -> A || AndBC = Result -> exists OrAB OrAC,
      (A || B = OrAB /\ A || C = OrAC) /\ OrAB && OrAC = Result

• or_bool__undistribute_over__and :

  forall A B C OrAB OrAC Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> extensibella:stdLib:is_bool C ->
    A || B = OrAB -> A || C = OrAC -> OrAB && OrAC = Result -> exists AndBC,
      B && C = AndBC /\ A || AndBC = Result

• DeMorgan__not_bool__and_bool :

  forall A B AndAB Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> A && B = AndAB -> ! AndAB = Result ->
    exists NotA NotB, (! A = NotA /\ ! B = NotB) /\ NotA || NotB = Result

• DeMorgan__or_bool__not_bool :

  forall A B NotA NotB Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> ! A = NotA -> ! B = NotB -> NotA || NotB = Result ->
    exists AndAB, A && B = AndAB /\ ! AndAB = Result

• DeMorgan__not_bool__or_bool :

  forall A B OrAB Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> A || B = OrAB -> ! OrAB = Result ->
    exists NotA NotB, (! A = NotA /\ ! B = NotB) /\ NotA && NotB = Result

• DeMorgan__and_bool__not_bool :

  forall A B NotA NotB Result,
    extensibella:stdLib:is_bool A -> extensibella:stdLib:is_bool B -> ! A = NotA -> ! B = NotB -> NotA && NotB = Result ->
    exists OrAB, A || B = OrAB /\ ! OrAB = Result

Integers

• is_integer_eq_or_not :

  forall I1 I2,
    extensibella:stdLib:is_integer I1 -> extensibella:stdLib:is_integer I2 -> I1 = I2 \/
    (I1 = I2 -> false)

ExtSize Induction

• all_acc :

  forall N,
    is_integer N -> 0 <= N -> extensibella:stdLib:acc N

• lt_left :

  forall A B C,
    A + B = C -> 0 <= A -> 0 <= B -> A < C \/ A = C

• lt_right :

  forall A B C,
    A + B = C -> is_integer B -> 0 <= A -> 0 <= B -> B < C \/ B = C

• lte_left :

  forall A B C,
    A + B = C -> is_integer A -> 0 <= A -> 0 <= B -> A <= C

• lte_right :

  forall A B C,
    A + B = C -> is_integer B -> 0 <= A -> 0 <= B -> B <= C

• lesseq_integer__add_positives :

  forall N1 N2 Sum,
    0 <= N1 -> 0 <= N2 -> N1 + N2 = Sum -> 0 <= Sum

• lt_plus_one :

  forall X Sum,
    1 + X = Sum -> is_integer X -> X < Sum