Stack Overflow
Stack Overflow

Questions tagged [proofs]

16 questions
21
votes
4 answers

Why is (a | b ) equivalent to a - (a & b) + b?

I was looking for a way to do a BITOR() with an Oracle database and came across a suggestion to just use BITAND() instead, replacing BITOR(a,b) with a + b - BITAND(a,b). I tested it by hand a few times and verified it seems to work for all binary…
Brandon Yarbrough
  • 37,021
  • 23
  • 116
  • 145
3
votes
1 answer

How do you use induction with tactics/Isar in Isabelle/HOL?

I am struggling to understand why each of the examples below either works or doesn't work and more abstractly how induction interacts with tactics vs Isar. I'm working on 4.3 in Programming and Proving in Isabelle/HOL (Dec 2016) on Windows 10 with…
neoDaedalus
  • 71
  • 6
2
votes
2 answers

Proving some monad laws on an error monad I wrote

So I whipped up a custom error monad and I was wondering how I would go about proving a few monad laws for it. If anyone is willing to take the time to help me out it would be much appreciated. Thanks! And here's my code: data Error a = Ok a | Error…
Cody Bonney
  • 1,648
  • 1
  • 10
  • 17
2
votes
1 answer

How to prove a Ada/SPARK precondition on a function embedded in a double loop

I'm trying to prove that the precondition of "prepend" holds during the execution of the program below. The precondition is: Length (Container) < Container.Capacity My attempts at proving this are in the code below in the form of pragmas. I can…
LT 'syreal' Jones
  • 97
  • 1
  • 9
2
votes
3 answers

Prove that n! is not in O(n^p) for any constant natural number p

How can I prove that n! is not in O(n^p) for any constant natural number p? And is (n k)(n choose k) in O(n^p), for all k?
user497302
1
vote
1 answer

Proving Big-Theta notation

Hello I've tried my best to understand big-theta and now I get the main conception of the proofs for Big-Oh and Big-Omega but i couldn't find and example that is close to my excercise, because i cant do the proof for that one: Prove, by exhibiting…
Zee
  • 2,240
  • 4
  • 18
  • 18
1
vote
0 answers

Proving the correctness of brute force maximum sub array algorithm

I am trying to prove the correctness of the brute force version of the maximum sub array problem given below: def max_subarray_bf(lst): left = 0 right = 0 max = lst[0] for i in range(len(lst)): current_sum=0 for j in…
Honda
  • 146
  • 6
1
vote
1 answer

proof of API response

Let's say I have access to an https weather API. Let's say I query its health status on thursday 17/08/2017 23h30 and the API replies OK (simple OK http code). As a client, I need to prove in the future that the service actually responded me this…
VsM
  • 710
  • 1
  • 10
  • 23
1
vote
1 answer

Z3 proofs: Are hypothesis and lemma rules always cleanly nested?

Quick question: In a Z3 proof (e.g. 4.3.2), a "hypothesis" rule introduces a local assumption, which is eventually discharged by a "lemma" rule. Are "hypothesis" and "lemma" rules always cleanly nested, meaning that one could map Z3 proofs to a…
Jasmin Blanchette
  • 56
  • 3
0
votes
1 answer

Associativity proof on Nats vs. Lists

I am comparing the associativity proofs for Nats and Lists. The proof on Lists goes by induction lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" by (induct xs) auto But, the proof on Nats is lemma nat_add_assoc: "(m + n) + k = m +…
Niki
  • 11
  • 1
0
votes
1 answer

How to prove a combination of asymptotic notations?

I think I have a good grasp of what Big O, omega, and theta notation means and how to prove if a function is one of them. I don't understand how to prove a combination of them, like in the problem. Could somebody explain this to me? Θ(n) + O(n^3) =…
helpmeeeee
  • 1
  • 1
0
votes
1 answer

Worst Case for stable matchings

In the stable matching problem, I am trying to generate the preference lists for worst case.I came across a paper that says this is the worst case for n=5 m1: w1 w2 w3 w4 w5 m2: w2 w3 w4 w1 w5 m3: w3 w4 w1 w2 w5 m4: w4 w1 w2 w3 w5 m5: w1 w2 w3 w4…
a_123
  • 183
  • 2
  • 13
0
votes
3 answers

Propositional Logic and Proofs

I am trying to prove the below case for a homework assignment and have been working hours on it, still no luck. Any suggestions or comments as to what I am doing wrong?
Eric Johnson
  • 47
  • 6
-1
votes
1 answer

Type inferencing help in OCaml

How would I proceed with proving these two functions are well typed? I am a bit lost with this question. let rec reduce f lst u = match lst with | [] -> u | (h::t) -> f h (reduce f t u) let rec forall2 p l1 l2 = match…
user3460123
  • 39
  • 4
-1
votes
1 answer

Partition of natural numbers in sets

How do I prove the following question Prove that in any partition of N9 (The first nine natural numbers) into three sets, there will be at least one set whose product of numbers is greater than or equal to 72.
user7917727
  • 1
1
2