adder/tests.py at master · dineshkumar227/adder · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
from transpiler import *


parsed_code = parse('∀ x, x ∈ A ∩ C → x ∈ A ∪ C', ['A', 'B', 'C'], ['x'], ['x ∈ (A) ∩ (C)'] , ['x ∈ (A) from assumption 1', 'x ∈ (A) ∪ (C) from statement 1'])
print()
print("===================Proof===================")
print()

for i in parsed_code:
	print(i)


parsed_code = parse('∀ x, x ∈ A ∩ C → x ∈ A', ['A', 'B', 'C'], ['x'], ['x ∈ (A) ∩ (C)'] , ['x ∈ (A) from assumption 1'])

print()
print("===================Proof===================")
print()

for i in parsed_code:
	print(i)

# wrong proof
parsed_code = parse('∀ x, x ∈ A → x ∈ A ∩ C', ['A', 'B', 'C'], ['x'], ['x ∈ (A)'] , ['x ∈ (A) ∩ (C) from assumption 1'])

print()
print("===================Proof===================")
print()

for i in parsed_code:
	print(i)